Theorem 3expia 1122

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 1121	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	expr 458	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  ad5ant125  1367  mp3an3  1451  3gencl  3518  moi  3714  disji  5131  disjord  5136  3optocl  5771  sossfld  6183  f1oresrab  7122  f1cdmsn  7277  soisores  7321  isomin  7331  isofrlem  7334  ovmpos  7553  ov2gf  7554  ndmovord  7594  nnsuc  7870  poxp  8111  frpoins3xp3g  8124  brtpos  8217  dfsmo2  8344  smoiun  8358  smoord  8362  smogt  8364  omeulem1  8579  omeu  8582  oewordi  8588  uniinqs  8788  mapvalg  8827  pmvalg  8828  elmapg  8830  xpdom3  9067  mapdom3  9146  sdomdomtrfi  9201  domsdomtrfi  9202  php  9207  php3  9209  nndomog  9213  php3OLD  9221  onomeneq  9225  sucdom  9232  unxpdomlem3  9249  isinf  9257  isinfOLD  9258  f1finf1o  9268  findcard2OLD  9281  isfinite2  9298  ordiso  9508  cnfcom3clem  9697  r111  9767  tskwe  9942  pr2ne  9996  pr2neOLD  9997  infxpenlem  10005  dfac8alem  10021  infdif  10201  infdif2  10202  cff1  10250  coflim  10253  cfslbn  10259  cfslb2n  10260  cofsmo  10261  cfsmolem  10262  cfcoflem  10264  fin23lem27  10320  isf32lem9  10353  isf34lem6  10372  axcc2lem  10428  domtriomlem  10434  axdc4lem  10447  zorn2lem2  10489  axdclem2  10512  konigthlem  10560  gchen1  10617  gchen2  10618  gchpwdom  10662  gchaleph  10663  winainflem  10685  tskcard  10773  gruiun  10791  gruen  10804  intgru  10806  grudomon  10809  grur1a  10811  grutsk1  10813  nqereu  10921  nqereq  10927  ltsonq  10961  prlem934  11025  reclem3pr  11041  1re  11211  axsup  11286  addlid  11394  recex  11843  lemul1a  12065  lt2msq  12096  fimaxre2  12156  zdiv  12629  zextlt  12633  prime  12640  uzind2  12652  fzind  12657  lbzbi  12917  qbtwnxr  13176  qextltlem  13178  xralrple  13181  xltneg  13193  xlt2add  13236  supxrgtmnf  13305  ixxub  13342  ixxlb  13343  ioo0  13346  ico0  13367  ioc0  13368  icc0  13369  iocssre  13401  icossre  13402  iccssre  13403  fzen  13515  expclzlem  14046  expaddz  14069  expmulz  14071  hashgadd  14334  hashunsngx  14350  hashgt23el  14381  elovmpowrd  14505  pfxnd0  14635  ccatopth2  14664  pfxccatin12  14680  cshf1  14757  shftuz  15013  cau3lem  15298  caubnd  15302  climuni  15493  lo1resb  15505  o1resb  15507  o1of2  15554  o1add  15555  o1mul  15556  o1sub  15557  ntrivcvgmul  15845  eflt  16057  moddvds  16205  dvdscmulr  16225  dvdsmulcr  16226  dvdsle  16250  divalglem8  16340  divalgb  16344  ndvdssub  16349  bitsfzo  16373  gcdcllem1  16437  gcdcllem3  16439  dvdsgcd  16483  lcmgcdlem  16540  lcmfeq0b  16564  qredeu  16592  isprm3  16617  prmdvdsexpr  16651  prmexpb  16654  eulerthlem2  16712  fermltl  16714  coprimeprodsq  16738  pythagtrip  16764  pcprendvds  16770  pcpremul  16773  pcdvdsb  16799  pc2dvds  16809  4sqlem12  16886  4sqlem18  16892  vdwlem10  16920  cshwshashlem3  17028  xpsrnbas  17514  ismred  17543  mrieqv2d  17580  iscatd  17614  isfuncd  17812  fthestrcsetc  18099  fthsetcestrc  18114  poslubd  18363  dirtr  18552  mulgaddcom  18973  ghmrn  19100  pmtrprfv3  19317  mndodcongi  19406  oddvdsnn0  19407  oddvds  19410  odcl2  19428  odhash3  19439  gexdvds  19447  pgpfi  19468  lsmss1b  19529  lsmss2b  19531  efgsrel  19597  efgred  19611  cntzcmn  19703  cyggenod  19747  lt6abl  19758  gsumcom2  19838  pgpfac1lem2  19940  pgpfac1lem3  19942  dvdsunit  20186  unitmulclb  20188  irredrmul  20234  isabvd  20421  lmodvsdi  20488  lss0cl  20550  islbs3  20761  lbsextlem2  20765  xrsdsreclblem  20984  psrbaglefi  21477  mvrf1  21537  coe1fzgsumd  21818  gsummoncoe1  21820  evl1gsumd  21868  scmataddcl  22010  scmatsubcl  22011  mdetunilem9  22114  mdetuni0  22115  mdetmul  22117  m2cpmrngiso  22252  pm2mpf1  22293  opnnei  22616  neindisj2  22619  cncls2  22769  cncls  22770  cnntr  22771  cnpresti  22784  cnprest  22785  lmcnp  22800  isreg2  22873  ordthauslem  22879  unconn  22925  2ndc1stc  22947  kgen2ss  23051  ptclsg  23111  cnmptcom  23174  kqfvima  23226  hmeof1o  23260  fbncp  23335  fbfinnfr  23337  trfbas2  23339  isufil2  23404  ufprim  23405  trufil  23406  filufint  23416  hausflim  23477  flimrest  23479  flimcls  23481  cnpfcf  23537  alexsubALT  23547  tmdgsum  23591  opnsubg  23604  cldsubg  23607  qustgpopn  23616  tsmsxp  23651  blpnf  23895  blssps  23922  blss  23923  blssec  23933  neibl  24002  prdsxmslem2  24030  xrsmopn  24320  metnrm  24370  climcncf  24408  iccpnfhmeo  24453  xrhmeo  24454  bndth  24466  cphsqrtcl3  24696  iscau2  24786  iscmet3lem2  24801  bcthlem5  24837  bcth3  24840  ishl2  24879  ivthlem1  24960  cmmbl  25043  iundisj2  25058  voliunlem2  25060  mbfaddlem  25169  itg2itg1  25246  itg2seq  25252  itg2mulclem  25256  cnplimc  25396  dvres2  25421  deg1nn0clb  25600  deg1lt0  25601  deg1ge  25608  plypf1  25718  plyadd  25723  plymul  25724  coeeu  25731  dgrub2  25741  coeidlem  25743  coeid3  25746  coemullem  25756  coe11  25759  coemulhi  25760  coemulc  25761  dgreq0  25771  dgrlt  25772  dgradd2  25774  vieta1lem2  25816  tanord1  26038  tanord  26039  logccne0  26079  cxpeq0  26178  cxpmul2z  26191  cxpcn3lem  26245  relogbzcl  26269  angpieqvd  26326  o1cxp  26469  scvxcvx  26480  chtublem  26704  bposlem3  26779  lgsqr  26844  2sqnn  26932  dchrisumlema  26981  dchrisumlem2  26983  ostth2lem3  27128  nosepon  27158  noextenddif  27161  nolesgn2o  27164  nogesgn1o  27166  nosepne  27173  nodense  27185  tghilberti2  27879  inagswap  28082  f1otrg  28112  brbtwn2  28153  axpasch  28189  axcontlem4  28215  axcontlem5  28216  upgredg2vtx  28391  usgredg2vtxeuALT  28469  sizusglecusg  28710  upgredginwlk  28883  frgrwopreg1  29561  frgrwopreg2  29562  frgrregorufrg  29569  lpni  29721  ipasslem5  30076  htthlem  30158  omlsii  30644  spansni  30798  spansneleq  30811  elspansn4  30814  sumspansn  30890  homco1  31042  homulass  31043  mdsl0  31551  ssdmd1  31554  ssdmd2  31555  cvdmd  31578  chirredlem2  31632  atdmd  31639  atmd2  31641  disjif  31797  iundisj2f  31809  isoun  31911  preiman0  31919  padct  31932  iocinioc2  31978  iundisj2fi  31996  archiabllem1a  32325  archiabllem2a  32328  slmdvsdi  32348  ordtconnlem1  32893  indpi1  33007  measinblem  33207  measres  33209  measdivcstALTV  33212  mbfmco2  33253  orvclteinc  33463  sgn3da  33529  sgnnbi  33533  sgnpbi  33534  bnj605  33907  bnj607  33916  bnj964  33943  bnj1033  33969  bnj1128  33990  bnj1137  33995  bnj1136  33997  bnj1413  34035  bnj60  34062  fineqvac  34086  cusgredgex  34101  subgrwlk  34112  acycgr1v  34129  cvmlift2lem10  34292  msubvrs  34540  wsuclem  34786  dfrdg4  34912  brcolinear2  35019  brsegle2  35070  nn0prpw  35197  ntruni  35201  clsint2  35203  fnessref  35231  fnemeet2  35241  fnejoin2  35243  limsucncmpi  35319  ee7.2aOLD  35335  bj-idreseq  36032  dissneqlem  36210  isbasisrelowllem1  36225  isbasisrelowllem2  36226  icoreclin  36227  poimirlem9  36486  poimirlem30  36507  poimirlem32  36509  areacirc  36570  filbcmb  36597  mettrifi  36614  heiborlem8  36675  heiborlem10  36677  heibor  36678  riscer  36845  igenval2  36923  lshpcmp  37847  eqlkr  37958  lkrlsp2  37962  lkrshp  37964  cvrnbtwn2  38134  cvlexch3  38191  cvlexch4N  38192  cvlatexchb1  38193  cvlsupr3  38203  exatleN  38264  cvratlem  38281  atcvrj2b  38292  cvrat3  38302  cvrat4  38303  athgt  38316  ps-1  38337  ps-2  38338  3atlem5  38347  3at  38350  llnneat  38374  llnmlplnN  38399  lplnneat  38405  lplnnelln  38406  islpln2a  38408  lplnriaN  38410  lplnribN  38411  lplnexllnN  38424  2llnjaN  38426  lvolnle3at  38442  lvolneatN  38448  lvolnelln  38449  lvolnelpln  38450  islvol2aN  38452  dalem62  38594  pmapglb2N  38631  pmapglb2xN  38632  lncmp  38643  paddasslem14  38693  paddasslem15  38694  pmod2iN  38709  hlmod1i  38716  pclfinclN  38810  osumcllem8N  38823  pexmidlem4N  38833  pl42lem1N  38839  pl42lem4N  38842  lhpexle1  38868  lhpexle2lem  38869  lhpmcvr5N  38887  lhpmcvr6N  38888  ltrneq  39009  trlnidatb  39037  cdleme0ex2N  39084  cdleme27a  39227  cdleme17d3  39356  cdlemeg46gfre  39392  cdleme48gfv1  39396  cdlemeg49lebilem  39399  cdlemf2  39422  cdlemf  39423  cdlemfnid  39424  trlord  39429  cdlemg31c  39559  cdlemg35  39573  trlcone  39588  tendoeq2  39634  cdlemj3  39683  cdlemk26b-3  39765  cdlemk33N  39769  cdleml3N  39838  cdlemn  40072  dih1dimb2  40101  dihord5apre  40122  dihmeetlem1N  40150  dihglblem5apreN  40151  dihglblem2N  40154  dihglblem3N  40155  dihmeetlem13N  40179  dihmeetlem15N  40181  dihatexv  40198  hdmap14lem12  40739  uzindd  40831  lcmineqlem1  40883  sticksstones1  40951  metakunt1  40974  metakunt5  40978  frlmfzowrdb  41076  nn0rppwr  41220  nn0expgcd  41222  dvdsexpnn0  41228  rtprmirr  41234  oddcomabszz  41669  jm2.19lem4  41717  fiuneneq  41925  idomsubgmo  41926  omcl2  42069  pwinfi3  42300  gneispa  42867  mnringmulrcld  42973  grumnudlem  43030  ismnushort  43046  binomcxplemnn0  43094  addrcom  43220  int3  43359  suctrALT  43573  suctrALTcf  43669  suctrALT3  43671  chordthmALT  43680  iunconnlem2  43682  stoweidlem26  44729  stoweidlem34  44737  issald  45036  goldbachth  46202  nnsgrp  46574  ply1mulgsumlem1  47021  lubsscl  47547  glbsscl  47548