Theorem 3expia 1259

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expia	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1256	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 444	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  mp3an3  1405  3gencl  3210  moi  3356  disji  4570  3optocl  5120  sossfld  5499  f1oresrab  6302  soisores  6477  isomin  6487  isofrlem  6490  ovmpt2s  6682  ov2gf  6683  ndmovord  6722  nnsuc  6974  poxp  7176  brtpos  7248  dfsmo2  7331  smoiun  7345  smoord  7349  smogt  7351  omeulem1  7549  omeu  7552  oewordi  7558  uniinqs  7714  mapvalg  7754  pmvalg  7755  elmapg  7757  xpdom3  7943  mapdom3  8017  php3  8031  unxpdomlem3  8051  isinf  8058  findcard2  8085  isfinite2  8103  ordiso  8304  cnfcom3clem  8485  r111  8521  tskwe  8659  pr2ne  8711  infxpenlem  8719  dfac8alem  8735  infdif  8914  infdif2  8915  cff1  8963  coflim  8966  cfslbn  8972  cfslb2n  8973  cofsmo  8974  cfsmolem  8975  cfcoflem  8977  fin23lem27  9033  isf32lem9  9066  isf34lem6  9085  axcc2lem  9141  domtriomlem  9147  axdc4lem  9160  zorn2lem2  9202  axdclem2  9225  konigthlem  9269  gchen1  9326  gchen2  9327  gchpwdom  9371  gchaleph  9372  winainflem  9394  tskcard  9482  gruiun  9500  gruen  9513  intgru  9515  grudomon  9518  grur1a  9520  grutsk1  9522  nqereu  9630  nqereq  9636  ltsonq  9670  prlem934  9734  reclem3pr  9750  1re  9918  axsup  9992  addid2  10098  recex  10538  lemul1a  10756  lt2msq  10787  fimaxre2  10848  zdiv  11323  zextlt  11327  prime  11334  uzind2  11346  fzind  11351  lbzbi  11652  qbtwnxr  11905  qextltlem  11907  xralrple  11910  xltneg  11922  xlt2add  11962  supxrgtmnf  12031  ixxub  12067  ixxlb  12068  ioo0  12071  ico0  12092  ioc0  12093  icc0  12094  iocssre  12124  icossre  12125  iccssre  12126  fzen  12229  expclzlem  12746  expaddz  12766  expmulz  12768  hashgadd  13027  elovmpt2wrd  13202  ccatopth2  13323  cshf1  13407  shftuz  13657  cau3lem  13942  caubnd  13946  climuni  14131  lo1resb  14143  o1resb  14145  o1of2  14191  o1add  14192  o1mul  14193  o1sub  14194  ntrivcvgmul  14473  eflt  14686  moddvds  14829  dvdscmulr  14848  dvdsmulcr  14849  dvdsle  14870  divalglem8  14961  divalgb  14965  ndvdssub  14971  bitsfzo  14995  gcdcllem1  15059  gcdcllem3  15061  dvdsgcd  15099  lcmgcdlem  15157  lcmfeq0b  15181  qredeu  15210  isprm3  15234  prmdvdsexpr  15267  prmexpb  15268  eulerthlem2  15325  fermltl  15327  coprimeprodsq  15351  pythagtrip  15377  pcprendvds  15383  pcpremul  15386  pcdvdsb  15411  pc2dvds  15421  4sqlem12  15498  4sqlem18  15504  vdwlem10  15532  cshwshashlem3  15642  xpslem  16056  ismred  16085  mrieqv2d  16122  iscatd  16157  isfuncd  16348  fthestrcsetc  16613  fthsetcestrc  16628  poslubd  16971  dirtr  17059  mulgaddcom  17387  ghmrn  17496  pmtrprfv3  17697  mndodcongi  17785  oddvdsnn0  17786  oddvds  17789  odcl2  17805  odhash3  17814  gexdvds  17822  pgpfi  17843  lsmss1b  17903  lsmss2b  17905  efgsrel  17970  efgred  17984  cntzcmn  18068  cyggenod  18109  lt6abl  18119  gsumcom2  18197  pgpfac1lem2  18297  pgpfac1lem3  18299  dvdsunit  18486  unitmulclb  18488  irredrmul  18530  isabvd  18643  lmodvsdi  18709  lss0cl  18768  islbs3  18976  lbsextlem2  18980  mvrf1  19246  coe1fzgsumd  19493  gsummoncoe1  19495  evl1gsumd  19542  xrsdsreclblem  19611  scmataddcl  20141  scmatsubcl  20142  mdetunilem9  20245  mdetuni0  20246  mdetmul  20248  m2cpmrngiso  20382  pm2mpf1  20423  opnnei  20734  neindisj2  20737  cncls2  20887  cncls  20888  cnntr  20889  cnpresti  20902  cnprest  20903  lmcnp  20918  isreg2  20991  ordthauslem  20997  uncon  21042  2ndc1stc  21064  kgen2ss  21168  ptclsg  21228  cnmptcom  21291  kqfvima  21343  hmeof1o  21377  fbncp  21453  fbfinnfr  21455  trfbas2  21457  isufil2  21522  ufprim  21523  trufil  21524  filufint  21534  hausflim  21595  flimrest  21597  flimcls  21599  cnpfcf  21655  alexsubALT  21665  tmdgsum  21709  opnsubg  21721  cldsubg  21724  qustgpopn  21733  tsmsxp  21768  blpnf  22012  blssps  22039  blss  22040  blssec  22050  neibl  22116  prdsxmslem2  22144  xrsmopn  22423  metnrm  22473  climcncf  22511  iccpnfhmeo  22552  xrhmeo  22553  bndth  22565  cphsqrtcl3  22795  iscau2  22883  iscmet3lem2  22898  bcthlem5  22933  bcth3  22936  ishl2  22974  ivthlem1  23027  cmmbl  23109  iundisj2  23124  voliunlem2  23126  mbfaddlem  23233  itg2itg1  23309  itg2seq  23315  itg2mulclem  23319  cnplimc  23457  dvres2  23482  deg1nn0clb  23654  deg1lt0  23655  deg1ge  23662  plypf1  23772  plyadd  23777  plymul  23778  coeeu  23785  dgrub2  23795  coeidlem  23797  coeid3  23800  coemullem  23810  coe11  23813  coemulhi  23814  coemulc  23815  dgreq0  23825  dgrlt  23826  dgradd2  23828  vieta1lem2  23870  tanord1  24087  tanord  24088  logccne0  24129  cxpeq0  24224  cxpmul2z  24237  cxpcn3lem  24288  relogbzcl  24312  angpieqvd  24358  o1cxp  24501  scvxcvx  24512  chtublem  24736  bposlem3  24811  lgsqr  24876  dchrisumlema  24977  dchrisumlem2  24979  ostth2lem3  25124  iscgrglt  25209  tghilberti2  25333  inagswap  25530  f1otrg  25551  brbtwn2  25585  axpasch  25621  axcontlem4  25647  axcontlem5  25648  upgredg2vtx  25814  sizeusglecusg  26014  wwlkextproplem3  26271  lpni  26722  ipasslem5  27074  htthlem  27158  omlsii  27646  spansni  27800  spansneleq  27813  elspansn4  27816  sumspansn  27892  homco1  28044  homulass  28045  mdsl0  28553  ssdmd1  28556  ssdmd2  28557  cvdmd  28580  chirredlem2  28634  atdmd  28641  atmd2  28643  disjif  28773  iundisj2f  28785  isoun  28862  padct  28885  iocinioc2  28931  iundisj2fi  28943  archiabllem1a  29076  archiabllem2a  29079  slmdvsdi  29099  ordtconlem1  29298  indpi1  29411  measinblem  29610  measres  29612  measdivcstOLD  29614  mbfmco2  29654  orvclteinc  29864  sgn3da  29930  sgnnbi  29934  sgnpbi  29935  bnj605  30231  bnj607  30240  bnj964  30267  bnj1033  30291  bnj1128  30312  bnj1137  30317  bnj1136  30319  bnj1413  30357  bnj60  30384  cvmlift2lem10  30548  msubvrs  30711  wsuclem  31017  wsuclemOLD  31018  nosepon  31066  nodense  31088  dfrdg4  31228  brcolinear2  31335  brsegle2  31386  nn0prpw  31488  ntruni  31492  clsint2  31494  fnessref  31522  fnemeet2  31532  fnejoin2  31534  limsucncmpi  31614  ee7.2aOLD  31630  dissneqlem  32363  isbasisrelowllem1  32379  isbasisrelowllem2  32380  icoreclin  32381  poimirlem9  32588  poimirlem30  32609  poimirlem32  32611  areacirc  32675  filbcmb  32705  mettrifi  32723  heiborlem8  32787  heiborlem10  32789  heibor  32790  riscer  32957  igenval2  33035  lshpcmp  33293  eqlkr  33404  lkrlsp2  33408  lkrshp  33410  cvrnbtwn2  33580  cvlexch3  33637  cvlexch4N  33638  cvlatexchb1  33639  cvlsupr3  33649  exatleN  33708  cvratlem  33725  atcvrj2b  33736  cvrat3  33746  cvrat4  33747  athgt  33760  ps-1  33781  ps-2  33782  3atlem5  33791  3at  33794  llnneat  33818  llnmlplnN  33843  lplnneat  33849  lplnnelln  33850  islpln2a  33852  lplnriaN  33854  lplnribN  33855  lplnexllnN  33868  2llnjaN  33870  lvolnle3at  33886  lvolneatN  33892  lvolnelln  33893  lvolnelpln  33894  islvol2aN  33896  dalem62  34038  pmapglb2N  34075  pmapglb2xN  34076  lncmp  34087  paddasslem14  34137  paddasslem15  34138  pmod2iN  34153  hlmod1i  34160  pclfinclN  34254  osumcllem8N  34267  pexmidlem4N  34277  pl42lem1N  34283  pl42lem4N  34286  lhpexle1  34312  lhpexle2lem  34313  lhpmcvr5N  34331  lhpmcvr6N  34332  ltrneq  34453  trlnidatb  34482  cdleme0ex2N  34529  cdleme27a  34673  cdleme17d3  34802  cdlemeg46gfre  34838  cdleme48gfv1  34842  cdlemeg49lebilem  34845  cdlemf2  34868  cdlemf  34869  cdlemfnid  34870  trlord  34875  cdlemg31c  35005  cdlemg35  35019  trlcone  35034  tendoeq2  35080  cdlemj3  35129  cdlemk26b-3  35211  cdlemk33N  35215  cdleml3N  35284  cdlemn  35519  dih1dimb2  35548  dihord5apre  35569  dihmeetlem1N  35597  dihglblem5apreN  35598  dihglblem2N  35601  dihglblem3N  35602  dihmeetlem13N  35626  dihmeetlem15N  35628  dihatexv  35645  hdmap14lem12  36189  oddcomabszz  36527  jm2.19lem4  36577  fiuneneq  36794  idomsubgmo  36795  pwinfi3  36887  gneispa  37448  binomcxplemnn0  37570  addrcom  37700  int3  37858  suctrALT  38083  suctrALTcf  38180  suctrALT3  38182  chordthmALT  38191  iunconlem2  38193  stoweidlem26  38919  stoweidlem34  38927  goldbachth  39997  usgredg2vtxeuALT  40449  sizusglecusg  40679  nnsgrp  41607  ply1mulgsumlem1  41968