Theorem 3expia 1119

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

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

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

This theorem is referenced by:  ad5ant125  1364  mp3an3  1447  3gencl  3513  moi  3711  disji  5125  disjord  5130  3optocl  5768  sossfld  6184  f1oresrab  7130  f1cdmsn  7285  soisores  7329  isomin  7339  isofrlem  7342  ovmpos  7563  ov2gf  7564  ndmovord  7605  nnsuc  7882  poxp  8127  frpoins3xp3g  8140  brtpos  8234  dfsmo2  8361  smoiun  8375  smoord  8379  smogt  8381  omeulem1  8596  omeu  8599  oewordi  8605  uniinqs  8807  mapvalg  8846  pmvalg  8847  elmapg  8849  xpdom3  9086  mapdom3  9165  sdomdomtrfi  9220  domsdomtrfi  9221  php  9226  php3  9228  nndomog  9232  php3OLD  9240  onomeneq  9244  sucdom  9251  unxpdomlem3  9268  isinf  9276  isinfOLD  9277  f1finf1o  9287  findcard2OLD  9300  isfinite2  9317  ordiso  9531  cnfcom3clem  9720  r111  9790  tskwe  9965  pr2ne  10019  pr2neOLD  10020  infxpenlem  10028  dfac8alem  10044  infdif  10224  infdif2  10225  cff1  10273  coflim  10276  cfslbn  10282  cfslb2n  10283  cofsmo  10284  cfsmolem  10285  cfcoflem  10287  fin23lem27  10343  isf32lem9  10376  isf34lem6  10395  axcc2lem  10451  domtriomlem  10457  axdc4lem  10470  zorn2lem2  10512  axdclem2  10535  konigthlem  10583  gchen1  10640  gchen2  10641  gchpwdom  10685  gchaleph  10686  winainflem  10708  tskcard  10796  gruiun  10814  gruen  10827  intgru  10829  grudomon  10832  grur1a  10834  grutsk1  10836  nqereu  10944  nqereq  10950  ltsonq  10984  prlem934  11048  reclem3pr  11064  1re  11236  axsup  11311  addlid  11419  recex  11868  lemul1a  12090  lt2msq  12121  fimaxre2  12181  zdiv  12654  zextlt  12658  prime  12665  uzind2  12677  fzind  12682  lbzbi  12942  qbtwnxr  13203  qextltlem  13205  xralrple  13208  xltneg  13220  xlt2add  13263  supxrgtmnf  13332  ixxub  13369  ixxlb  13370  ioo0  13373  ico0  13394  ioc0  13395  icc0  13396  iocssre  13428  icossre  13429  iccssre  13430  fzen  13542  expclzlem  14072  expaddz  14095  expmulz  14097  hashgadd  14360  hashunsngx  14376  hashgt23el  14407  elovmpowrd  14532  pfxnd0  14662  ccatopth2  14691  pfxccatin12  14707  cshf1  14784  shftuz  15040  cau3lem  15325  caubnd  15329  climuni  15520  lo1resb  15532  o1resb  15534  o1of2  15581  o1add  15582  o1mul  15583  o1sub  15584  ntrivcvgmul  15872  eflt  16085  moddvds  16233  dvdscmulr  16253  dvdsmulcr  16254  dvdsle  16278  divalglem8  16368  divalgb  16372  ndvdssub  16377  bitsfzo  16401  gcdcllem1  16465  gcdcllem3  16467  dvdsgcd  16511  lcmgcdlem  16568  lcmfeq0b  16592  qredeu  16620  isprm3  16645  prmdvdsexpr  16679  prmexpb  16682  eulerthlem2  16742  fermltl  16744  coprimeprodsq  16768  pythagtrip  16794  pcprendvds  16800  pcpremul  16803  pcdvdsb  16829  pc2dvds  16839  4sqlem12  16916  4sqlem18  16922  vdwlem10  16950  cshwshashlem3  17058  xpsrnbas  17544  ismred  17573  mrieqv2d  17610  iscatd  17644  isfuncd  17842  fthestrcsetc  18132  fthsetcestrc  18147  poslubd  18396  dirtr  18585  mulgaddcom  19044  ghmrn  19174  pmtrprfv3  19400  mndodcongi  19489  oddvdsnn0  19490  oddvds  19493  odcl2  19511  odhash3  19522  gexdvds  19530  pgpfi  19551  lsmss1b  19612  lsmss2b  19614  efgsrel  19680  efgred  19694  cntzcmn  19786  cyggenod  19830  lt6abl  19841  gsumcom2  19921  pgpfac1lem2  20023  pgpfac1lem3  20025  dvdsunit  20307  unitmulclb  20309  irredrmul  20355  isabvd  20689  lmodvsdi  20757  lss0cl  20820  islbs3  21032  lbsextlem2  21036  xrsdsreclblem  21332  psrbaglefi  21852  mvrf1  21915  coe1fzgsumd  22210  gsummoncoe1  22214  evl1gsumd  22263  scmataddcl  22405  scmatsubcl  22406  mdetunilem9  22509  mdetuni0  22510  mdetmul  22512  m2cpmrngiso  22647  pm2mpf1  22688  opnnei  23011  neindisj2  23014  cncls2  23164  cncls  23165  cnntr  23166  cnpresti  23179  cnprest  23180  lmcnp  23195  isreg2  23268  ordthauslem  23274  unconn  23320  2ndc1stc  23342  kgen2ss  23446  ptclsg  23506  cnmptcom  23569  kqfvima  23621  hmeof1o  23655  fbncp  23730  fbfinnfr  23732  trfbas2  23734  isufil2  23799  ufprim  23800  trufil  23801  filufint  23811  hausflim  23872  flimrest  23874  flimcls  23876  cnpfcf  23932  alexsubALT  23942  tmdgsum  23986  opnsubg  23999  cldsubg  24002  qustgpopn  24011  tsmsxp  24046  blpnf  24290  blssps  24317  blss  24318  blssec  24328  neibl  24397  prdsxmslem2  24425  xrsmopn  24715  metnrm  24765  climcncf  24807  iccpnfhmeo  24857  xrhmeo  24858  bndth  24871  cphsqrtcl3  25102  iscau2  25192  iscmet3lem2  25207  bcthlem5  25243  bcth3  25246  ishl2  25285  ivthlem1  25367  cmmbl  25450  iundisj2  25465  voliunlem2  25467  mbfaddlem  25576  itg2itg1  25653  itg2seq  25659  itg2mulclem  25663  cnplimc  25803  dvres2  25828  deg1nn0clb  26013  deg1lt0  26014  deg1ge  26021  plypf1  26133  plyadd  26138  plymul  26139  coeeu  26146  dgrub2  26156  coeidlem  26158  coeid3  26161  coemullem  26171  coe11  26174  coemulhi  26175  coemulc  26176  dgreq0  26187  dgrlt  26188  dgradd2  26190  vieta1lem2  26233  tanord1  26458  tanord  26459  logccne0  26499  cxpeq0  26599  cxpmul2z  26612  cxpcn3lem  26669  relogbzcl  26693  angpieqvd  26750  o1cxp  26894  scvxcvx  26905  chtublem  27131  bposlem3  27206  lgsqr  27271  2sqnn  27359  dchrisumlema  27408  dchrisumlem2  27410  ostth2lem3  27555  nosepon  27585  noextenddif  27588  nolesgn2o  27591  nogesgn1o  27593  nosepne  27600  nodense  27612  tghilberti2  28429  inagswap  28632  f1otrg  28662  brbtwn2  28703  axpasch  28739  axcontlem4  28765  axcontlem5  28766  upgredg2vtx  28941  usgredg2vtxeuALT  29022  sizusglecusg  29264  upgredginwlk  29437  frgrwopreg1  30115  frgrwopreg2  30116  frgrregorufrg  30123  lpni  30277  ipasslem5  30632  htthlem  30714  omlsii  31200  spansni  31354  spansneleq  31367  elspansn4  31370  sumspansn  31446  homco1  31598  homulass  31599  mdsl0  32107  ssdmd1  32110  ssdmd2  32111  cvdmd  32134  chirredlem2  32188  atdmd  32195  atmd2  32197  disjif  32353  iundisj2f  32365  isoun  32465  preiman0  32473  padct  32485  iocinioc2  32531  iundisj2fi  32549  archiabllem1a  32877  archiabllem2a  32880  slmdvsdi  32900  ordtconnlem1  33461  indpi1  33575  measinblem  33775  measres  33777  measdivcstALTV  33780  mbfmco2  33821  orvclteinc  34031  sgn3da  34097  sgnnbi  34101  sgnpbi  34102  bnj605  34474  bnj607  34483  bnj964  34510  bnj1033  34536  bnj1128  34557  bnj1137  34562  bnj1136  34564  bnj1413  34602  bnj60  34629  fineqvac  34653  cusgredgex  34667  subgrwlk  34678  acycgr1v  34695  cvmlift2lem10  34858  msubvrs  35106  wsuclem  35357  dfrdg4  35483  brcolinear2  35590  brsegle2  35641  nn0prpw  35743  ntruni  35747  clsint2  35749  fnessref  35777  fnemeet2  35787  fnejoin2  35789  limsucncmpi  35865  ee7.2aOLD  35881  bj-idreseq  36577  dissneqlem  36755  isbasisrelowllem1  36770  isbasisrelowllem2  36771  icoreclin  36772  poimirlem9  37037  poimirlem30  37058  poimirlem32  37060  areacirc  37121  filbcmb  37148  mettrifi  37165  heiborlem8  37226  heiborlem10  37228  heibor  37229  riscer  37396  igenval2  37474  lshpcmp  38397  eqlkr  38508  lkrlsp2  38512  lkrshp  38514  cvrnbtwn2  38684  cvlexch3  38741  cvlexch4N  38742  cvlatexchb1  38743  cvlsupr3  38753  exatleN  38814  cvratlem  38831  atcvrj2b  38842  cvrat3  38852  cvrat4  38853  athgt  38866  ps-1  38887  ps-2  38888  3atlem5  38897  3at  38900  llnneat  38924  llnmlplnN  38949  lplnneat  38955  lplnnelln  38956  islpln2a  38958  lplnriaN  38960  lplnribN  38961  lplnexllnN  38974  2llnjaN  38976  lvolnle3at  38992  lvolneatN  38998  lvolnelln  38999  lvolnelpln  39000  islvol2aN  39002  dalem62  39144  pmapglb2N  39181  pmapglb2xN  39182  lncmp  39193  paddasslem14  39243  paddasslem15  39244  pmod2iN  39259  hlmod1i  39266  pclfinclN  39360  osumcllem8N  39373  pexmidlem4N  39383  pl42lem1N  39389  pl42lem4N  39392  lhpexle1  39418  lhpexle2lem  39419  lhpmcvr5N  39437  lhpmcvr6N  39438  ltrneq  39559  trlnidatb  39587  cdleme0ex2N  39634  cdleme27a  39777  cdleme17d3  39906  cdlemeg46gfre  39942  cdleme48gfv1  39946  cdlemeg49lebilem  39949  cdlemf2  39972  cdlemf  39973  cdlemfnid  39974  trlord  39979  cdlemg31c  40109  cdlemg35  40123  trlcone  40138  tendoeq2  40184  cdlemj3  40233  cdlemk26b-3  40315  cdlemk33N  40319  cdleml3N  40388  cdlemn  40622  dih1dimb2  40651  dihord5apre  40672  dihmeetlem1N  40700  dihglblem5apreN  40701  dihglblem2N  40704  dihglblem3N  40705  dihmeetlem13N  40729  dihmeetlem15N  40731  dihatexv  40748  hdmap14lem12  41289  uzindd  41384  lcmineqlem1  41437  sticksstones1  41550  metakunt1  41577  metakunt5  41581  frlmfzowrdb  41664  nn0rppwr  41815  nn0expgcd  41817  dvdsexpnn0  41823  rtprmirr  41828  oddcomabszz  42287  jm2.19lem4  42335  fiuneneq  42542  idomsubgmo  42543  omcl2  42685  pwinfi3  42916  gneispa  43483  mnringmulrcld  43588  grumnudlem  43645  ismnushort  43661  binomcxplemnn0  43709  addrcom  43835  int3  43974  suctrALT  44188  suctrALTcf  44284  suctrALT3  44286  chordthmALT  44295  iunconnlem2  44297  stoweidlem26  45337  stoweidlem34  45345  issald  45644  goldbachth  46810  nnsgrp  47162  ply1mulgsumlem1  47377  lubsscl  47902  glbsscl  47903