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  1392  mp3an3  1480  3gencl  3497  vtocl3gaf  3543  vtocl3ga  3544  moi  3679  disji  5093  disjord  5097  3optocl  5756  sossfld  6196  f1oresrab  7160  f1cdmsn  7321  soisores  7366  isomin  7376  isofrlem  7379  ovmpos  7600  ov2gf  7601  ndmovord  7643  nnsuc  7929  poxp  8177  frpoins3xp3g  8195  brtpos  8290  dfsmo2  8393  smoiun  8407  smoord  8411  smogt  8413  omeulem1  8628  omeu  8631  oewordi  8638  uniinqs  8856  mapvalg  8894  pmvalg  8895  elmapg  8897  xpdom3  9132  mapdom3  9206  sdomdomtrfi  9254  domsdomtrfi  9255  php  9260  php3  9262  nndomog  9266  onomeneq  9267  sucdom  9273  unxpdomlem3  9287  isinf  9294  f1finf1o  9302  isfinite2  9328  prfi  9353  ordiso  9547  cnfcom3clem  9743  r111  9819  tskwe  10068  pr2ne  10123  infxpenlem  10131  dfac8alem  10147  infdif  10325  infdif2  10326  cff1  10375  coflim  10378  cfslbn  10384  cfslb2n  10385  cofsmo  10386  cfsmolem  10387  cfcoflem  10389  fin23lem27  10445  isf32lem9  10478  isf34lem6  10497  axcc2lem  10553  domtriomlem  10559  axdc4lem  10572  zorn2lem2  10614  axdclem2  10637  konigthlem  10692  gchen1  10749  gchen2  10750  gchpwdom  10794  gchaleph  10795  winainflem  10817  tskcard  10905  gruiun  10923  gruen  10936  intgru  10938  grudomon  10941  grur1a  10943  grutsk1  10945  nqereu  11053  nqereq  11059  ltsonq  11093  prlem934  11157  reclem3pr  11173  1re  11347  axsup  11424  addlid  11532  recex  11988  lemul1a  12211  lt2msq  12242  fimaxre2  12302  indpi1  12374  zdiv  12809  zextlt  12813  prime  12820  uzind2  12832  fzind  12837  lbzbi  13103  qbtwnxr  13370  qextltlem  13372  xralrple  13375  xltneg  13387  xlt2add  13430  supxrgtmnf  13499  ixxub  13537  ixxlb  13538  ioo0  13541  ico0  13562  ioc0  13563  icc0  13564  iocssre  13598  icossre  13599  iccssre  13600  fzen  13714  expclzlem  14266  expaddz  14289  expmulz  14291  hashgadd  14562  hashunsngx  14578  hashgt23el  14610  elovmpowrd  14744  pfxnd0  14880  ccatopth2  14908  pfxccatin12  14924  cshf1  15003  shftuz  15265  sgn3da  15297  sgnnbi  15300  sgnpbi  15301  cau3lem  15566  caubnd  15570  climuni  15763  lo1resb  15775  o1resb  15777  o1of2  15824  o1add  15825  o1mul  15826  o1sub  15827  ntrivcvgmul  16115  eflt  16329  moddvds  16477  dvdscmulr  16498  dvdsmulcr  16499  dvdsle  16524  divalglem8  16614  divalgb  16618  ndvdssub  16623  bitsfzo  16649  gcdcllem1  16713  gcdcllem3  16715  dvdsgcd  16761  nn0rppwr  16779  nn0expgcd  16782  lcmgcdlem  16825  lcmfeq0b  16849  qredeu  16877  isprm3  16902  prmdvdsexpr  16937  prmexpb  16939  eulerthlem2  17003  fermltl  17005  coprimeprodsq  17030  pythagtrip  17056  pcprendvds  17062  pcpremul  17065  pcdvdsb  17091  pc2dvds  17101  4sqlem12  17178  4sqlem18  17184  vdwlem10  17212  cshwshashlem3  17319  xpsrnbas  17793  ismred  17822  mrieqv2d  17863  iscatd  17897  isfuncd  18090  fthestrcsetc  18374  fthsetcestrc  18389  poslubd  18635  dirtr  18826  mulgaddcom  19358  ghmrn  19493  pmtrprfv3  19719  mndodcongi  19808  oddvdsnn0  19809  oddvds  19812  odcl2  19830  odhash3  19841  gexdvds  19849  pgpfi  19870  lsmss1b  19931  lsmss2b  19933  efgsrel  19999  efgred  20013  cntzcmn  20105  cyggenod  20149  lt6abl  20160  gsumcom2  20240  pgpfac1lem2  20342  pgpfac1lem3  20344  dvdsunit  20660  unitmulclb  20662  irredrmul  20708  isabvd  21120  lmodvsdi  21211  lss0cl  21273  islbs3  21484  lbsextlem2  21488  rspprop  21575  xrsdsreclblem  21771  psrbaglefi  22289  mvrf1  22348  coe1fzgsumd  22677  gsummoncoe1  22681  evl1gsumd  22730  scmataddcl  22886  scmatsubcl  22887  mdetunilem9  22990  mdetuni0  22991  mdetmul  22993  m2cpmrngiso  23131  pm2mpf1  23172  opnnei  23493  neindisj2  23496  cncls2  23646  cncls  23647  cnntr  23648  cnpresti  23661  cnprest  23662  lmcnp  23677  isreg2  23750  ordthauslem  23756  unconn  23802  2ndc1stc  23824  kgen2ss  23929  ptclsg  23989  cnmptcom  24052  kqfvima  24104  hmeof1o  24138  fbncp  24213  fbfinnfr  24215  trfbas2  24217  isufil2  24282  ufprim  24283  trufil  24284  filufint  24294  hausflim  24355  flimrest  24357  flimcls  24359  cnpfcf  24415  alexsubALT  24425  tmdgsum  24469  opnsubg  24482  cldsubg  24485  qustgpopn  24494  tsmsxp  24529  blpnf  24771  blssps  24798  blss  24799  blssec  24809  neibl  24875  prdsxmslem2  24903  xrsmopn  25187  metnrm  25237  climcncf  25276  iccpnfhmeo  25321  xrhmeo  25322  bndth  25334  cphsqrtcl3  25563  iscau2  25653  iscmet3lem2  25668  bcthlem5  25704  bcth3  25707  ishl2  25746  ivthlem1  25827  cmmbl  25910  iundisj2  25925  voliunlem2  25927  mbfaddlem  26036  itg2itg1  26112  itg2seq  26118  itg2mulclem  26122  cnplimc  26262  dvres2  26287  deg1nn0clb  26463  deg1lt0  26464  deg1ge  26471  plypf1  26586  plyadd  26591  plymul  26592  coeeu  26599  dgrub2  26609  coeidlem  26611  coeid3  26614  coemullem  26624  coe11  26627  coemulhi  26628  coemulc  26629  dgreq0  26639  dgrlt  26640  dgradd2  26642  vieta1lem2  26689  tanord1  26922  tanord  26923  logccne0  26963  cxpeq0  27063  cxpmul2z  27076  cxpcn3lem  27132  rtprmirr  27145  relogbzcl  27159  angpieqvd  27216  o1cxp  27359  scvxcvx  27370  chtublem  27595  bposlem3  27670  lgsqr  27735  2sqnn  27823  dchrisumlema  27872  dchrisumlem2  27874  ostth2lem3  28019  nosepon  28079  noextenddif  28082  nolesgn2o  28085  nogesgn1o  28087  nosepne  28094  nodense  28106  onnolt  28709  onlts  28710  oniso  28714  bdayn0p1  28812  bdayn0sf1o  28813  tghilberti2  29163  inagswap  29417  f1otrg  29505  brbtwn2  29540  axpasch  29576  axcontlem4  29602  axcontlem5  29603  upgredg2vtx  29776  usgredg2vtxeuALT  29860  sizusglecusg  30101  upgredginwlk  30273  subgrwlk  30326  frgrwopreg1  30976  frgrwopreg2  30977  frgrregorufrg  30984  lpni  31139  ipasslem5  31494  htthlem  31576  omlsii  32062  spansni  32216  spansneleq  32229  elspansn4  32232  sumspansn  32308  homco1  32460  homulass  32461  mdsl0  32969  ssdmd1  32972  ssdmd2  32973  cvdmd  32996  chirredlem2  33050  atdmd  33057  atmd2  33059  disjif  33270  iundisj2f  33282  acunirnmpt2f  33353  isoun  33392  preiman0  33400  padct  33407  iocinioc2  33467  iundisj2fi  33485  archiabllem1a  33851  archiabllem2a  33854  slmdvsdi  33875  ordtconnlem1  34667  measinblem  34964  measres  34966  measdivcstALTV  34969  mbfmco2  35008  orvclteinc  35219  bnj605  35648  bnj607  35657  bnj964  35684  bnj1033  35710  bnj1128  35731  bnj1137  35736  bnj1136  35738  bnj1413  35776  bnj60  35803  soinfdom  35841  rankfilimb  35853  r1filim  35854  nelscottrankgt  35874  erscottd  35884  weexenwe  35889  acwer1prc  35893  fineqvac  35925  fineqvnttrclselem3  35932  fineqvnttrclse  35933  j0ltaleph  36049  jf1  36051  onprcf1acwevdlem1  36086  onprcf1acwevd  36088  vonf1oonfo  36090  cusgredgex  36104  acycgr1v  36112  cvmlift2lem10  36285  msubvrs  36533  elpssmo  36673  wsuclem  36802  dfrdg4  36930  brcolinear2  37038  brsegle2  37089  nn0prpw  37326  ntruni  37330  clsint2  37332  fnessref  37360  fnemeet2  37370  fnejoin2  37372  limsucncmpi  37448  ee7.2aOLD  37464  bj-idreseq  38351  dissneqlem  38531  isbasisrelowllem1  38546  isbasisrelowllem2  38547  icoreclin  38548  poimirlem9  38815  poimirlem30  38836  poimirlem32  38838  areacirc  38899  filbcmb  38940  mettrifi  38957  heiborlem8  39018  heiborlem10  39020  heibor  39021  riscer  39188  igenval2  39266  eldisjim3  40013  eldisjs6  40138  lshpcmp  40311  eqlkr  40422  lkrlsp2  40426  lkrshp  40428  cvrnbtwn2  40598  cvlexch3  40655  cvlexch4N  40656  cvlatexchb1  40657  cvlsupr3  40667  exatleN  40727  cvratlem  40744  atcvrj2b  40755  cvrat3  40765  cvrat4  40766  athgt  40779  ps-1  40800  ps-2  40801  3atlem5  40810  3at  40813  llnneat  40837  llnmlplnN  40862  lplnneat  40868  lplnnelln  40869  islpln2a  40871  lplnriaN  40873  lplnribN  40874  lplnexllnN  40887  2llnjaN  40889  lvolnle3at  40905  lvolneatN  40911  lvolnelln  40912  lvolnelpln  40913  islvol2aN  40915  dalem62  41057  pmapglb2N  41094  pmapglb2xN  41095  lncmp  41106  paddasslem14  41156  paddasslem15  41157  pmod2iN  41172  hlmod1i  41179  pclfinclN  41273  osumcllem8N  41286  pexmidlem4N  41296  pl42lem1N  41302  pl42lem4N  41305  lhpexle1  41331  lhpexle2lem  41332  lhpmcvr5N  41350  lhpmcvr6N  41351  ltrneq  41472  trlnidatb  41500  cdleme0ex2N  41547  cdleme27a  41690  cdleme17d3  41819  cdlemeg46gfre  41855  cdleme48gfv1  41859  cdlemeg49lebilem  41862  cdlemf2  41885  cdlemf  41886  cdlemfnid  41887  trlord  41892  cdlemg31c  42022  cdlemg35  42036  trlcone  42051  tendoeq2  42097  cdlemj3  42146  cdlemk26b-3  42228  cdlemk33N  42232  cdleml3N  42301  cdlemn  42535  dih1dimb2  42564  dihord5apre  42585  dihmeetlem1N  42613  dihglblem5apreN  42614  dihglblem2N  42617  dihglblem3N  42618  dihmeetlem13N  42642  dihmeetlem15N  42644  dihatexv  42661  hdmap14lem12  43202  uzindd  43294  lcmineqlem1  43345  sticksstones1  43462  dvdsexpnn0  43652  frlmfzowrdb  43837  oddcomabszz  44217  jm2.19lem4  44265  fiuneneq  44455  idomsubgmo  44456  omcl2  44596  pwinfi3  44825  gneispa  45391  mnringmulrcld  45487  grumnudlem  45530  ismnushort  45546  binomcxplemnn0  45594  addrcom  45717  int3  45855  suctrALT  46068  suctrALTcf  46164  suctrALT3  46166  chordthmALT  46175  iunconnlem2  46177  relpmin  46206  relpfrlem  46207  stoweidlem26  47309  stoweidlem34  47317  issald  47616  goldbachth  48905  nprmdvdsfacm1  48982  grlimgrtri  49374  nnsgrp  49547  ply1mulgsumlem1  49829  lubsscl  50405  glbsscl  50406