Theorem 3expia 1120

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ad5ant125  1365  mp3an3  1449  3gencl  3523  vtocl3gaf  3581  vtocl3ga  3583  moi  3727  disji  5133  disjord  5137  3optocl  5785  sossfld  6208  f1oresrab  7147  f1cdmsn  7302  soisores  7347  isomin  7357  isofrlem  7360  ovmpos  7581  ov2gf  7582  ndmovord  7623  nnsuc  7905  poxp  8152  frpoins3xp3g  8165  brtpos  8259  dfsmo2  8386  smoiun  8400  smoord  8404  smogt  8406  omeulem1  8619  omeu  8622  oewordi  8628  uniinqs  8836  mapvalg  8875  pmvalg  8876  elmapg  8878  xpdom3  9109  mapdom3  9188  sdomdomtrfi  9239  domsdomtrfi  9240  php  9245  php3  9247  nndomog  9251  php3OLD  9259  onomeneq  9263  sucdom  9269  unxpdomlem3  9286  isinf  9294  isinfOLD  9295  f1finf1o  9303  isfinite2  9332  prfi  9361  ordiso  9554  cnfcom3clem  9743  r111  9813  tskwe  9988  pr2ne  10042  pr2neOLD  10043  infxpenlem  10051  dfac8alem  10067  infdif  10246  infdif2  10247  cff1  10296  coflim  10299  cfslbn  10305  cfslb2n  10306  cofsmo  10307  cfsmolem  10308  cfcoflem  10310  fin23lem27  10366  isf32lem9  10399  isf34lem6  10418  axcc2lem  10474  domtriomlem  10480  axdc4lem  10493  zorn2lem2  10535  axdclem2  10558  konigthlem  10606  gchen1  10663  gchen2  10664  gchpwdom  10708  gchaleph  10709  winainflem  10731  tskcard  10819  gruiun  10837  gruen  10850  intgru  10852  grudomon  10855  grur1a  10857  grutsk1  10859  nqereu  10967  nqereq  10973  ltsonq  11007  prlem934  11071  reclem3pr  11087  1re  11259  axsup  11334  addlid  11442  recex  11893  lemul1a  12119  lt2msq  12151  fimaxre2  12211  zdiv  12686  zextlt  12690  prime  12697  uzind2  12709  fzind  12714  lbzbi  12976  qbtwnxr  13239  qextltlem  13241  xralrple  13244  xltneg  13256  xlt2add  13299  supxrgtmnf  13368  ixxub  13405  ixxlb  13406  ioo0  13409  ico0  13430  ioc0  13431  icc0  13432  iocssre  13464  icossre  13465  iccssre  13466  fzen  13578  expclzlem  14121  expaddz  14144  expmulz  14146  hashgadd  14413  hashunsngx  14429  hashgt23el  14460  elovmpowrd  14593  pfxnd0  14723  ccatopth2  14752  pfxccatin12  14768  cshf1  14845  shftuz  15105  cau3lem  15390  caubnd  15394  climuni  15585  lo1resb  15597  o1resb  15599  o1of2  15646  o1add  15647  o1mul  15648  o1sub  15649  ntrivcvgmul  15935  eflt  16150  moddvds  16298  dvdscmulr  16319  dvdsmulcr  16320  dvdsle  16344  divalglem8  16434  divalgb  16438  ndvdssub  16443  bitsfzo  16469  gcdcllem1  16533  gcdcllem3  16535  dvdsgcd  16578  nn0rppwr  16595  nn0expgcd  16598  lcmgcdlem  16640  lcmfeq0b  16664  qredeu  16692  isprm3  16717  prmdvdsexpr  16751  prmexpb  16753  eulerthlem2  16816  fermltl  16818  coprimeprodsq  16842  pythagtrip  16868  pcprendvds  16874  pcpremul  16877  pcdvdsb  16903  pc2dvds  16913  4sqlem12  16990  4sqlem18  16996  vdwlem10  17024  cshwshashlem3  17132  xpsrnbas  17618  ismred  17647  mrieqv2d  17684  iscatd  17718  isfuncd  17916  fthestrcsetc  18206  fthsetcestrc  18221  poslubd  18471  dirtr  18660  mulgaddcom  19129  ghmrn  19260  pmtrprfv3  19487  mndodcongi  19576  oddvdsnn0  19577  oddvds  19580  odcl2  19598  odhash3  19609  gexdvds  19617  pgpfi  19638  lsmss1b  19699  lsmss2b  19701  efgsrel  19767  efgred  19781  cntzcmn  19873  cyggenod  19917  lt6abl  19928  gsumcom2  20008  pgpfac1lem2  20110  pgpfac1lem3  20112  dvdsunit  20396  unitmulclb  20398  irredrmul  20444  isabvd  20830  lmodvsdi  20900  lss0cl  20963  islbs3  21175  lbsextlem2  21179  xrsdsreclblem  21448  psrbaglefi  21964  mvrf1  22024  coe1fzgsumd  22324  gsummoncoe1  22328  evl1gsumd  22377  scmataddcl  22538  scmatsubcl  22539  mdetunilem9  22642  mdetuni0  22643  mdetmul  22645  m2cpmrngiso  22780  pm2mpf1  22821  opnnei  23144  neindisj2  23147  cncls2  23297  cncls  23298  cnntr  23299  cnpresti  23312  cnprest  23313  lmcnp  23328  isreg2  23401  ordthauslem  23407  unconn  23453  2ndc1stc  23475  kgen2ss  23579  ptclsg  23639  cnmptcom  23702  kqfvima  23754  hmeof1o  23788  fbncp  23863  fbfinnfr  23865  trfbas2  23867  isufil2  23932  ufprim  23933  trufil  23934  filufint  23944  hausflim  24005  flimrest  24007  flimcls  24009  cnpfcf  24065  alexsubALT  24075  tmdgsum  24119  opnsubg  24132  cldsubg  24135  qustgpopn  24144  tsmsxp  24179  blpnf  24423  blssps  24450  blss  24451  blssec  24461  neibl  24530  prdsxmslem2  24558  xrsmopn  24848  metnrm  24898  climcncf  24940  iccpnfhmeo  24990  xrhmeo  24991  bndth  25004  cphsqrtcl3  25235  iscau2  25325  iscmet3lem2  25340  bcthlem5  25376  bcth3  25379  ishl2  25418  ivthlem1  25500  cmmbl  25583  iundisj2  25598  voliunlem2  25600  mbfaddlem  25709  itg2itg1  25786  itg2seq  25792  itg2mulclem  25796  cnplimc  25937  dvres2  25962  deg1nn0clb  26144  deg1lt0  26145  deg1ge  26152  plypf1  26266  plyadd  26271  plymul  26272  coeeu  26279  dgrub2  26289  coeidlem  26291  coeid3  26294  coemullem  26304  coe11  26307  coemulhi  26308  coemulc  26309  dgreq0  26320  dgrlt  26321  dgradd2  26323  vieta1lem2  26368  tanord1  26594  tanord  26595  logccne0  26635  cxpeq0  26735  cxpmul2z  26748  cxpcn3lem  26805  rtprmirr  26818  relogbzcl  26832  angpieqvd  26889  o1cxp  27033  scvxcvx  27044  chtublem  27270  bposlem3  27345  lgsqr  27410  2sqnn  27498  dchrisumlema  27547  dchrisumlem2  27549  ostth2lem3  27694  nosepon  27725  noextenddif  27728  nolesgn2o  27731  nogesgn1o  27733  nosepne  27740  nodense  27752  tghilberti2  28661  inagswap  28864  f1otrg  28894  brbtwn2  28935  axpasch  28971  axcontlem4  28997  axcontlem5  28998  upgredg2vtx  29173  usgredg2vtxeuALT  29254  sizusglecusg  29496  upgredginwlk  29669  frgrwopreg1  30347  frgrwopreg2  30348  frgrregorufrg  30355  lpni  30509  ipasslem5  30864  htthlem  30946  omlsii  31432  spansni  31586  spansneleq  31599  elspansn4  31602  sumspansn  31678  homco1  31830  homulass  31831  mdsl0  32339  ssdmd1  32342  ssdmd2  32343  cvdmd  32366  chirredlem2  32420  atdmd  32427  atmd2  32429  disjif  32598  iundisj2f  32610  isoun  32717  preiman0  32725  padct  32737  iocinioc2  32788  iundisj2fi  32805  archiabllem1a  33181  archiabllem2a  33184  slmdvsdi  33204  ordtconnlem1  33885  indpi1  34001  measinblem  34201  measres  34203  measdivcstALTV  34206  mbfmco2  34247  orvclteinc  34457  sgn3da  34523  sgnnbi  34527  sgnpbi  34528  bnj605  34900  bnj607  34909  bnj964  34936  bnj1033  34962  bnj1128  34983  bnj1137  34988  bnj1136  34990  bnj1413  35028  bnj60  35055  fineqvac  35090  cusgredgex  35106  subgrwlk  35117  acycgr1v  35134  cvmlift2lem10  35297  msubvrs  35545  wsuclem  35807  dfrdg4  35933  brcolinear2  36040  brsegle2  36091  nn0prpw  36306  ntruni  36310  clsint2  36312  fnessref  36340  fnemeet2  36350  fnejoin2  36352  limsucncmpi  36428  ee7.2aOLD  36444  bj-idreseq  37145  dissneqlem  37323  isbasisrelowllem1  37338  isbasisrelowllem2  37339  icoreclin  37340  poimirlem9  37616  poimirlem30  37637  poimirlem32  37639  areacirc  37700  filbcmb  37727  mettrifi  37744  heiborlem8  37805  heiborlem10  37807  heibor  37808  riscer  37975  igenval2  38053  lshpcmp  38970  eqlkr  39081  lkrlsp2  39085  lkrshp  39087  cvrnbtwn2  39257  cvlexch3  39314  cvlexch4N  39315  cvlatexchb1  39316  cvlsupr3  39326  exatleN  39387  cvratlem  39404  atcvrj2b  39415  cvrat3  39425  cvrat4  39426  athgt  39439  ps-1  39460  ps-2  39461  3atlem5  39470  3at  39473  llnneat  39497  llnmlplnN  39522  lplnneat  39528  lplnnelln  39529  islpln2a  39531  lplnriaN  39533  lplnribN  39534  lplnexllnN  39547  2llnjaN  39549  lvolnle3at  39565  lvolneatN  39571  lvolnelln  39572  lvolnelpln  39573  islvol2aN  39575  dalem62  39717  pmapglb2N  39754  pmapglb2xN  39755  lncmp  39766  paddasslem14  39816  paddasslem15  39817  pmod2iN  39832  hlmod1i  39839  pclfinclN  39933  osumcllem8N  39946  pexmidlem4N  39956  pl42lem1N  39962  pl42lem4N  39965  lhpexle1  39991  lhpexle2lem  39992  lhpmcvr5N  40010  lhpmcvr6N  40011  ltrneq  40132  trlnidatb  40160  cdleme0ex2N  40207  cdleme27a  40350  cdleme17d3  40479  cdlemeg46gfre  40515  cdleme48gfv1  40519  cdlemeg49lebilem  40522  cdlemf2  40545  cdlemf  40546  cdlemfnid  40547  trlord  40552  cdlemg31c  40682  cdlemg35  40696  trlcone  40711  tendoeq2  40757  cdlemj3  40806  cdlemk26b-3  40888  cdlemk33N  40892  cdleml3N  40961  cdlemn  41195  dih1dimb2  41224  dihord5apre  41245  dihmeetlem1N  41273  dihglblem5apreN  41274  dihglblem2N  41277  dihglblem3N  41278  dihmeetlem13N  41302  dihmeetlem15N  41304  dihatexv  41321  hdmap14lem12  41862  uzindd  41959  lcmineqlem1  42011  sticksstones1  42128  metakunt1  42187  metakunt5  42191  dvdsexpnn0  42348  frlmfzowrdb  42491  oddcomabszz  42933  jm2.19lem4  42981  fiuneneq  43181  idomsubgmo  43182  omcl2  43323  pwinfi3  43553  gneispa  44120  mnringmulrcld  44224  grumnudlem  44281  ismnushort  44297  binomcxplemnn0  44345  addrcom  44471  int3  44610  suctrALT  44824  suctrALTcf  44920  suctrALT3  44922  chordthmALT  44931  iunconnlem2  44933  stoweidlem26  45982  stoweidlem34  45990  issald  46289  goldbachth  47472  grlimgrtri  47899  nnsgrp  48021  ply1mulgsumlem1  48232  lubsscl  48757  glbsscl  48758