Theorem 3expia 1139

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) (Proof shortened by Wolf Lammen, 22-Jun-2022.)

Hypothesis

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

Assertion

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

Proof of Theorem 3expia

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1138	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	expr 462	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ad5ant125OLD  1391  mp3an3  1479  3gencl  3500  vtocl3gaf  3546  vtocl3ga  3547  moi  3683  disji  5096  disjord  5100  3optocl  5760  sossfld  6186  f1oresrab  7127  f1cdmsn  7286  soisores  7331  isomin  7341  isofrlem  7344  ovmpos  7564  ov2gf  7565  ndmovord  7606  nnsuc  7882  poxp  8126  frpoins3xp3g  8139  brtpos  8233  dfsmo2  8336  smoiun  8350  smoord  8354  smogt  8356  omeulem1  8569  omeu  8572  oewordi  8579  uniinqs  8797  mapvalg  8835  pmvalg  8836  elmapg  8838  xpdom3  9066  mapdom3  9140  sdomdomtrfi  9188  domsdomtrfi  9189  php  9194  php3  9196  nndomog  9200  onomeneq  9201  sucdom  9207  unxpdomlem3  9221  isinf  9228  f1finf1o  9236  isfinite2  9261  prfi  9286  ordiso  9481  cnfcom3clem  9677  r111  9750  tskwe  9948  pr2ne  10001  infxpenlem  10009  dfac8alem  10025  infdif  10203  infdif2  10204  cff1  10253  coflim  10256  cfslbn  10262  cfslb2n  10263  cofsmo  10264  cfsmolem  10265  cfcoflem  10267  fin23lem27  10323  isf32lem9  10356  isf34lem6  10375  axcc2lem  10431  domtriomlem  10437  axdc4lem  10450  zorn2lem2  10492  axdclem2  10515  konigthlem  10564  gchen1  10621  gchen2  10622  gchpwdom  10666  gchaleph  10667  winainflem  10689  tskcard  10777  gruiun  10795  gruen  10808  intgru  10810  grudomon  10813  grur1a  10815  grutsk1  10817  nqereu  10925  nqereq  10931  ltsonq  10965  prlem934  11029  reclem3pr  11045  1re  11219  axsup  11296  addlid  11404  recex  11857  lemul1a  12080  lt2msq  12111  fimaxre2  12171  indpi1  12243  zdiv  12678  zextlt  12682  prime  12689  uzind2  12701  fzind  12706  lbzbi  12972  qbtwnxr  13238  qextltlem  13240  xralrple  13243  xltneg  13255  xlt2add  13298  supxrgtmnf  13367  ixxub  13405  ixxlb  13406  ioo0  13409  ico0  13430  ioc0  13431  icc0  13432  iocssre  13466  icossre  13467  iccssre  13468  fzen  13581  expclzlem  14133  expaddz  14156  expmulz  14158  hashgadd  14427  hashunsngx  14443  hashgt23el  14475  elovmpowrd  14609  pfxnd0  14744  ccatopth2  14772  pfxccatin12  14788  cshf1  14867  shftuz  15126  sgn3da  15158  sgnnbi  15161  sgnpbi  15162  cau3lem  15426  caubnd  15430  climuni  15623  lo1resb  15635  o1resb  15637  o1of2  15684  o1add  15685  o1mul  15686  o1sub  15687  ntrivcvgmul  15975  eflt  16191  moddvds  16339  dvdscmulr  16360  dvdsmulcr  16361  dvdsle  16386  divalglem8  16476  divalgb  16480  ndvdssub  16485  bitsfzo  16511  gcdcllem1  16575  gcdcllem3  16577  dvdsgcd  16620  nn0rppwr  16637  nn0expgcd  16640  lcmgcdlem  16682  lcmfeq0b  16706  qredeu  16734  isprm3  16759  prmdvdsexpr  16794  prmexpb  16796  eulerthlem2  16859  fermltl  16861  coprimeprodsq  16886  pythagtrip  16912  pcprendvds  16918  pcpremul  16921  pcdvdsb  16947  pc2dvds  16957  4sqlem12  17034  4sqlem18  17040  vdwlem10  17068  cshwshashlem3  17175  xpsrnbas  17643  ismred  17672  mrieqv2d  17713  iscatd  17747  isfuncd  17940  fthestrcsetc  18224  fthsetcestrc  18239  poslubd  18485  dirtr  18676  mulgaddcom  19188  ghmrn  19323  pmtrprfv3  19548  mndodcongi  19637  oddvdsnn0  19638  oddvds  19641  odcl2  19659  odhash3  19670  gexdvds  19678  pgpfi  19699  lsmss1b  19760  lsmss2b  19762  efgsrel  19828  efgred  19842  cntzcmn  19934  cyggenod  19978  lt6abl  19989  gsumcom2  20069  pgpfac1lem2  20171  pgpfac1lem3  20173  dvdsunit  20487  unitmulclb  20489  irredrmul  20535  isabvd  20945  lmodvsdi  21036  lss0cl  21098  islbs3  21309  lbsextlem2  21313  rspprop  21400  xrsdsreclblem  21593  psrbaglefi  22106  mvrf1  22165  coe1fzgsumd  22494  gsummoncoe1  22498  evl1gsumd  22547  scmataddcl  22703  scmatsubcl  22704  mdetunilem9  22807  mdetuni0  22808  mdetmul  22810  m2cpmrngiso  22945  pm2mpf1  22986  opnnei  23307  neindisj2  23310  cncls2  23460  cncls  23461  cnntr  23462  cnpresti  23475  cnprest  23476  lmcnp  23491  isreg2  23564  ordthauslem  23570  unconn  23616  2ndc1stc  23638  kgen2ss  23743  ptclsg  23803  cnmptcom  23866  kqfvima  23918  hmeof1o  23952  fbncp  24027  fbfinnfr  24029  trfbas2  24031  isufil2  24096  ufprim  24097  trufil  24098  filufint  24108  hausflim  24169  flimrest  24171  flimcls  24173  cnpfcf  24229  alexsubALT  24239  tmdgsum  24283  opnsubg  24296  cldsubg  24299  qustgpopn  24308  tsmsxp  24343  blpnf  24585  blssps  24612  blss  24613  blssec  24623  neibl  24689  prdsxmslem2  24717  xrsmopn  25001  metnrm  25051  climcncf  25090  iccpnfhmeo  25135  xrhmeo  25136  bndth  25148  cphsqrtcl3  25377  iscau2  25467  iscmet3lem2  25482  bcthlem5  25518  bcth3  25521  ishl2  25560  ivthlem1  25641  cmmbl  25724  iundisj2  25739  voliunlem2  25741  mbfaddlem  25850  itg2itg1  25926  itg2seq  25932  itg2mulclem  25936  cnplimc  26077  dvres2  26102  deg1nn0clb  26278  deg1lt0  26279  deg1ge  26286  plypf1  26400  plyadd  26405  plymul  26406  coeeu  26413  dgrub2  26423  coeidlem  26425  coeid3  26428  coemullem  26438  coe11  26441  coemulhi  26442  coemulc  26443  dgreq0  26453  dgrlt  26454  dgradd2  26456  vieta1lem2  26503  tanord1  26733  tanord  26734  logccne0  26774  cxpeq0  26874  cxpmul2z  26887  cxpcn3lem  26943  rtprmirr  26956  relogbzcl  26970  angpieqvd  27027  o1cxp  27170  scvxcvx  27181  chtublem  27406  bposlem3  27481  lgsqr  27546  2sqnn  27634  dchrisumlema  27683  dchrisumlem2  27685  ostth2lem3  27830  nosepon  27860  noextenddif  27863  nolesgn2o  27866  nogesgn1o  27868  nosepne  27875  nodense  27887  onnolt  28490  onlts  28491  oniso  28495  bdayn0p1  28593  bdayn0sf1o  28594  tghilberti2  28942  inagswap  29189  f1otrg  29251  brbtwn2  29286  axpasch  29322  axcontlem4  29348  axcontlem5  29349  upgredg2vtx  29522  usgredg2vtxeuALT  29606  sizusglecusg  29847  upgredginwlk  30019  subgrwlk  30072  frgrwopreg1  30716  frgrwopreg2  30717  frgrregorufrg  30724  lpni  30879  ipasslem5  31234  htthlem  31316  omlsii  31802  spansni  31956  spansneleq  31969  elspansn4  31972  sumspansn  32048  homco1  32200  homulass  32201  mdsl0  32709  ssdmd1  32712  ssdmd2  32713  cvdmd  32736  chirredlem2  32790  atdmd  32797  atmd2  32799  disjif  32970  iundisj2f  32982  isoun  33094  preiman0  33102  padct  33109  iocinioc2  33170  iundisj2fi  33188  archiabllem1a  33551  archiabllem2a  33554  slmdvsdi  33575  ordtconnlem1  34354  measinblem  34651  measres  34653  measdivcstALTV  34656  mbfmco2  34696  orvclteinc  34907  bnj605  35336  bnj607  35345  bnj964  35372  bnj1033  35398  bnj1128  35419  bnj1137  35424  bnj1136  35426  bnj1413  35464  bnj60  35491  rankfilimb  35530  r1filim  35532  nelscottrankgt  35552  fineqvac  35562  fineqvnttrclselem3  35569  fineqvnttrclse  35570  vonf1oonfo  35632  cusgredgex  35640  acycgr1v  35654  cvmlift2lem10  35817  msubvrs  36065  wsuclem  36328  dfrdg4  36456  brcolinear2  36563  brsegle2  36614  nn0prpw  36867  ntruni  36871  clsint2  36873  fnessref  36901  fnemeet2  36911  fnejoin2  36913  limsucncmpi  36989  ee7.2aOLD  37005  bj-idreseq  37839  dissneqlem  38019  isbasisrelowllem1  38034  isbasisrelowllem2  38035  icoreclin  38036  poimirlem9  38313  poimirlem30  38334  poimirlem32  38336  areacirc  38397  filbcmb  38424  mettrifi  38441  heiborlem8  38502  heiborlem10  38504  heibor  38505  riscer  38672  igenval2  38750  eldisjim3  39497  eldisjs6  39622  lshpcmp  39795  eqlkr  39906  lkrlsp2  39910  lkrshp  39912  cvrnbtwn2  40082  cvlexch3  40139  cvlexch4N  40140  cvlatexchb1  40141  cvlsupr3  40151  exatleN  40211  cvratlem  40228  atcvrj2b  40239  cvrat3  40249  cvrat4  40250  athgt  40263  ps-1  40284  ps-2  40285  3atlem5  40294  3at  40297  llnneat  40321  llnmlplnN  40346  lplnneat  40352  lplnnelln  40353  islpln2a  40355  lplnriaN  40357  lplnribN  40358  lplnexllnN  40371  2llnjaN  40373  lvolnle3at  40389  lvolneatN  40395  lvolnelln  40396  lvolnelpln  40397  islvol2aN  40399  dalem62  40541  pmapglb2N  40578  pmapglb2xN  40579  lncmp  40590  paddasslem14  40640  paddasslem15  40641  pmod2iN  40656  hlmod1i  40663  pclfinclN  40757  osumcllem8N  40770  pexmidlem4N  40780  pl42lem1N  40786  pl42lem4N  40789  lhpexle1  40815  lhpexle2lem  40816  lhpmcvr5N  40834  lhpmcvr6N  40835  ltrneq  40956  trlnidatb  40984  cdleme0ex2N  41031  cdleme27a  41174  cdleme17d3  41303  cdlemeg46gfre  41339  cdleme48gfv1  41343  cdlemeg49lebilem  41346  cdlemf2  41369  cdlemf  41370  cdlemfnid  41371  trlord  41376  cdlemg31c  41506  cdlemg35  41520  trlcone  41535  tendoeq2  41581  cdlemj3  41630  cdlemk26b-3  41712  cdlemk33N  41716  cdleml3N  41785  cdlemn  42019  dih1dimb2  42048  dihord5apre  42069  dihmeetlem1N  42097  dihglblem5apreN  42098  dihglblem2N  42101  dihglblem3N  42102  dihmeetlem13N  42126  dihmeetlem15N  42128  dihatexv  42145  hdmap14lem12  42686  uzindd  42778  lcmineqlem1  42829  sticksstones1  42946  dvdsexpnn0  43128  frlmfzowrdb  43311  oddcomabszz  43704  jm2.19lem4  43752  fiuneneq  43952  idomsubgmo  43953  omcl2  44093  pwinfi3  44322  gneispa  44889  mnringmulrcld  44985  grumnudlem  45028  ismnushort  45044  binomcxplemnn0  45092  addrcom  45216  int3  45354  suctrALT  45567  suctrALTcf  45663  suctrALT3  45665  chordthmALT  45674  iunconnlem2  45676  relpmin  45694  relpfrlem  45695  stoweidlem26  46773  stoweidlem34  46781  issald  47080  goldbachth  48332  nprmdvdsfacm1  48409  grlimgrtri  48801  nnsgrp  48975  ply1mulgsumlem1  49199  lubsscl  49771  glbsscl  49772