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  3494  vtocl3gaf  3540  vtocl3ga  3541  moi  3676  disji  5088  disjord  5092  3optocl  5748  sossfld  6178  f1oresrab  7126  f1cdmsn  7288  soisores  7333  isomin  7343  isofrlem  7346  ovmpos  7566  ov2gf  7567  ndmovord  7609  nnsuc  7893  poxp  8138  frpoins3xp3g  8151  brtpos  8245  dfsmo2  8348  smoiun  8362  smoord  8366  smogt  8368  omeulem1  8583  omeu  8586  oewordi  8593  uniinqs  8811  mapvalg  8849  pmvalg  8850  elmapg  8852  xpdom3  9087  mapdom3  9161  sdomdomtrfi  9209  domsdomtrfi  9210  php  9215  php3  9217  nndomog  9221  onomeneq  9222  sucdom  9228  unxpdomlem3  9242  isinf  9249  f1finf1o  9257  isfinite2  9283  prfi  9308  ordiso  9503  cnfcom3clem  9699  r111  9775  tskwe  10024  pr2ne  10077  infxpenlem  10085  dfac8alem  10101  infdif  10279  infdif2  10280  cff1  10329  coflim  10332  cfslbn  10338  cfslb2n  10339  cofsmo  10340  cfsmolem  10341  cfcoflem  10343  fin23lem27  10399  isf32lem9  10432  isf34lem6  10451  axcc2lem  10507  domtriomlem  10513  axdc4lem  10526  zorn2lem2  10568  axdclem2  10591  konigthlem  10646  gchen1  10703  gchen2  10704  gchpwdom  10748  gchaleph  10749  winainflem  10771  tskcard  10859  gruiun  10877  gruen  10890  intgru  10892  grudomon  10895  grur1a  10897  grutsk1  10899  nqereu  11007  nqereq  11013  ltsonq  11047  prlem934  11111  reclem3pr  11127  1re  11301  axsup  11378  addlid  11486  recex  11941  lemul1a  12164  lt2msq  12195  fimaxre2  12255  indpi1  12327  zdiv  12762  zextlt  12766  prime  12773  uzind2  12785  fzind  12790  lbzbi  13056  qbtwnxr  13323  qextltlem  13325  xralrple  13328  xltneg  13340  xlt2add  13383  supxrgtmnf  13452  ixxub  13490  ixxlb  13491  ioo0  13494  ico0  13515  ioc0  13516  icc0  13517  iocssre  13551  icossre  13552  iccssre  13553  fzen  13667  expclzlem  14219  expaddz  14242  expmulz  14244  hashgadd  14514  hashunsngx  14530  hashgt23el  14562  elovmpowrd  14696  pfxnd0  14831  ccatopth2  14859  pfxccatin12  14875  cshf1  14954  shftuz  15215  sgn3da  15247  sgnnbi  15250  sgnpbi  15251  cau3lem  15515  caubnd  15519  climuni  15712  lo1resb  15724  o1resb  15726  o1of2  15773  o1add  15774  o1mul  15775  o1sub  15776  ntrivcvgmul  16064  eflt  16278  moddvds  16426  dvdscmulr  16447  dvdsmulcr  16448  dvdsle  16473  divalglem8  16563  divalgb  16567  ndvdssub  16572  bitsfzo  16598  gcdcllem1  16662  gcdcllem3  16664  dvdsgcd  16710  nn0rppwr  16728  nn0expgcd  16731  lcmgcdlem  16774  lcmfeq0b  16798  qredeu  16826  isprm3  16851  prmdvdsexpr  16886  prmexpb  16888  eulerthlem2  16952  fermltl  16954  coprimeprodsq  16979  pythagtrip  17005  pcprendvds  17011  pcpremul  17014  pcdvdsb  17040  pc2dvds  17050  4sqlem12  17127  4sqlem18  17133  vdwlem10  17161  cshwshashlem3  17268  xpsrnbas  17736  ismred  17765  mrieqv2d  17806  iscatd  17840  isfuncd  18033  fthestrcsetc  18317  fthsetcestrc  18332  poslubd  18578  dirtr  18769  mulgaddcom  19301  ghmrn  19436  pmtrprfv3  19661  mndodcongi  19750  oddvdsnn0  19751  oddvds  19754  odcl2  19772  odhash3  19783  gexdvds  19791  pgpfi  19812  lsmss1b  19873  lsmss2b  19875  efgsrel  19941  efgred  19955  cntzcmn  20047  cyggenod  20091  lt6abl  20102  gsumcom2  20182  pgpfac1lem2  20284  pgpfac1lem3  20286  dvdsunit  20602  unitmulclb  20604  irredrmul  20650  isabvd  21062  lmodvsdi  21153  lss0cl  21215  islbs3  21426  lbsextlem2  21430  rspprop  21517  xrsdsreclblem  21712  psrbaglefi  22227  mvrf1  22286  coe1fzgsumd  22615  gsummoncoe1  22619  evl1gsumd  22668  scmataddcl  22824  scmatsubcl  22825  mdetunilem9  22928  mdetuni0  22929  mdetmul  22931  m2cpmrngiso  23069  pm2mpf1  23110  opnnei  23431  neindisj2  23434  cncls2  23584  cncls  23585  cnntr  23586  cnpresti  23599  cnprest  23600  lmcnp  23615  isreg2  23688  ordthauslem  23694  unconn  23740  2ndc1stc  23762  kgen2ss  23867  ptclsg  23927  cnmptcom  23990  kqfvima  24042  hmeof1o  24076  fbncp  24151  fbfinnfr  24153  trfbas2  24155  isufil2  24220  ufprim  24221  trufil  24222  filufint  24232  hausflim  24293  flimrest  24295  flimcls  24297  cnpfcf  24353  alexsubALT  24363  tmdgsum  24407  opnsubg  24420  cldsubg  24423  qustgpopn  24432  tsmsxp  24467  blpnf  24709  blssps  24736  blss  24737  blssec  24747  neibl  24813  prdsxmslem2  24841  xrsmopn  25125  metnrm  25175  climcncf  25214  iccpnfhmeo  25259  xrhmeo  25260  bndth  25272  cphsqrtcl3  25501  iscau2  25591  iscmet3lem2  25606  bcthlem5  25642  bcth3  25645  ishl2  25684  ivthlem1  25765  cmmbl  25848  iundisj2  25863  voliunlem2  25865  mbfaddlem  25974  itg2itg1  26050  itg2seq  26056  itg2mulclem  26060  cnplimc  26200  dvres2  26225  deg1nn0clb  26401  deg1lt0  26402  deg1ge  26409  plypf1  26524  plyadd  26529  plymul  26530  coeeu  26537  dgrub2  26547  coeidlem  26549  coeid3  26552  coemullem  26562  coe11  26565  coemulhi  26566  coemulc  26567  dgreq0  26577  dgrlt  26578  dgradd2  26580  vieta1lem2  26627  tanord1  26858  tanord  26859  logccne0  26899  cxpeq0  26999  cxpmul2z  27012  cxpcn3lem  27068  rtprmirr  27081  relogbzcl  27095  angpieqvd  27152  o1cxp  27295  scvxcvx  27306  chtublem  27531  bposlem3  27606  lgsqr  27671  2sqnn  27759  dchrisumlema  27808  dchrisumlem2  27810  ostth2lem3  27955  nosepon  28015  noextenddif  28018  nolesgn2o  28021  nogesgn1o  28023  nosepne  28030  nodense  28042  onnolt  28645  onlts  28646  oniso  28650  bdayn0p1  28748  bdayn0sf1o  28749  tghilberti2  29099  inagswap  29353  f1otrg  29441  brbtwn2  29476  axpasch  29512  axcontlem4  29538  axcontlem5  29539  upgredg2vtx  29712  usgredg2vtxeuALT  29796  sizusglecusg  30037  upgredginwlk  30209  subgrwlk  30262  frgrwopreg1  30912  frgrwopreg2  30913  frgrregorufrg  30920  lpni  31075  ipasslem5  31430  htthlem  31512  omlsii  31998  spansni  32152  spansneleq  32165  elspansn4  32168  sumspansn  32244  homco1  32396  homulass  32397  mdsl0  32905  ssdmd1  32908  ssdmd2  32909  cvdmd  32932  chirredlem2  32986  atdmd  32993  atmd2  32995  disjif  33165  iundisj2f  33177  isoun  33288  preiman0  33296  padct  33303  iocinioc2  33364  iundisj2fi  33382  archiabllem1a  33745  archiabllem2a  33748  slmdvsdi  33769  ordtconnlem1  34549  measinblem  34846  measres  34848  measdivcstALTV  34851  mbfmco2  34890  orvclteinc  35101  bnj605  35530  bnj607  35539  bnj964  35566  bnj1033  35592  bnj1128  35613  bnj1137  35618  bnj1136  35620  bnj1413  35658  bnj60  35685  rankfilimb  35717  r1filim  35718  nelscottrankgt  35737  fineqvac  35767  fineqvnttrclselem3  35774  fineqvnttrclse  35775  vonf1oonfo  35877  cusgredgex  35885  acycgr1v  35893  cvmlift2lem10  36056  msubvrs  36304  wsuclem  36567  dfrdg4  36695  brcolinear2  36803  brsegle2  36854  nn0prpw  37091  ntruni  37095  clsint2  37097  fnessref  37125  fnemeet2  37135  fnejoin2  37137  limsucncmpi  37213  ee7.2aOLD  37229  bj-idreseq  38063  dissneqlem  38243  isbasisrelowllem1  38258  isbasisrelowllem2  38259  icoreclin  38260  poimirlem9  38527  poimirlem30  38548  poimirlem32  38550  areacirc  38611  filbcmb  38654  mettrifi  38671  heiborlem8  38732  heiborlem10  38734  heibor  38735  riscer  38902  igenval2  38980  eldisjim3  39727  eldisjs6  39852  lshpcmp  40025  eqlkr  40136  lkrlsp2  40140  lkrshp  40142  cvrnbtwn2  40312  cvlexch3  40369  cvlexch4N  40370  cvlatexchb1  40371  cvlsupr3  40381  exatleN  40441  cvratlem  40458  atcvrj2b  40469  cvrat3  40479  cvrat4  40480  athgt  40493  ps-1  40514  ps-2  40515  3atlem5  40524  3at  40527  llnneat  40551  llnmlplnN  40576  lplnneat  40582  lplnnelln  40583  islpln2a  40585  lplnriaN  40587  lplnribN  40588  lplnexllnN  40601  2llnjaN  40603  lvolnle3at  40619  lvolneatN  40625  lvolnelln  40626  lvolnelpln  40627  islvol2aN  40629  dalem62  40771  pmapglb2N  40808  pmapglb2xN  40809  lncmp  40820  paddasslem14  40870  paddasslem15  40871  pmod2iN  40886  hlmod1i  40893  pclfinclN  40987  osumcllem8N  41000  pexmidlem4N  41010  pl42lem1N  41016  pl42lem4N  41019  lhpexle1  41045  lhpexle2lem  41046  lhpmcvr5N  41064  lhpmcvr6N  41065  ltrneq  41186  trlnidatb  41214  cdleme0ex2N  41261  cdleme27a  41404  cdleme17d3  41533  cdlemeg46gfre  41569  cdleme48gfv1  41573  cdlemeg49lebilem  41576  cdlemf2  41599  cdlemf  41600  cdlemfnid  41601  trlord  41606  cdlemg31c  41736  cdlemg35  41750  trlcone  41765  tendoeq2  41811  cdlemj3  41860  cdlemk26b-3  41942  cdlemk33N  41946  cdleml3N  42015  cdlemn  42249  dih1dimb2  42278  dihord5apre  42299  dihmeetlem1N  42327  dihglblem5apreN  42328  dihglblem2N  42331  dihglblem3N  42332  dihmeetlem13N  42356  dihmeetlem15N  42358  dihatexv  42375  hdmap14lem12  42916  uzindd  43008  lcmineqlem1  43059  sticksstones1  43176  dvdsexpnn0  43366  frlmfzowrdb  43551  oddcomabszz  43930  jm2.19lem4  43978  fiuneneq  44178  idomsubgmo  44179  omcl2  44319  pwinfi3  44548  gneispa  45115  mnringmulrcld  45211  grumnudlem  45254  ismnushort  45270  binomcxplemnn0  45318  addrcom  45442  int3  45580  suctrALT  45793  suctrALTcf  45889  suctrALT3  45891  chordthmALT  45900  iunconnlem2  45902  relpmin  45920  relpfrlem  45921  stoweidlem26  47005  stoweidlem34  47013  issald  47312  goldbachth  48601  nprmdvdsfacm1  48678  grlimgrtri  49070  nnsgrp  49243  ply1mulgsumlem1  49467  lubsscl  50037  glbsscl  50038