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 461	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 400   ∧ 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 210  df-an 401  df-3an 1087

This theorem is referenced by:  ad5ant125  1364  mp3an3  1448  3gencl  3453  moi  3633  disji  5016  disjord  5021  3optocl  5617  sossfld  6016  f1oresrab  6881  soisores  7075  isomin  7085  isofrlem  7088  ovmpos  7294  ov2gf  7295  ndmovord  7335  nnsuc  7597  poxp  7828  brtpos  7912  dfsmo2  7995  smoiun  8009  smoord  8013  smogt  8015  omeulem1  8219  omeu  8222  oewordi  8228  uniinqs  8388  mapvalg  8427  pmvalg  8428  elmapg  8430  xpdom3  8636  mapdom3  8711  php3  8725  unxpdomlem3  8746  isinf  8753  findcard2OLD  8784  isfinite2  8802  ordiso  9006  cnfcom3clem  9194  r111  9230  tskwe  9405  pr2ne  9458  infxpenlem  9466  dfac8alem  9482  infdif  9662  infdif2  9663  cff1  9711  coflim  9714  cfslbn  9720  cfslb2n  9721  cofsmo  9722  cfsmolem  9723  cfcoflem  9725  fin23lem27  9781  isf32lem9  9814  isf34lem6  9833  axcc2lem  9889  domtriomlem  9895  axdc4lem  9908  zorn2lem2  9950  axdclem2  9973  konigthlem  10021  gchen1  10078  gchen2  10079  gchpwdom  10123  gchaleph  10124  winainflem  10146  tskcard  10234  gruiun  10252  gruen  10265  intgru  10267  grudomon  10270  grur1a  10272  grutsk1  10274  nqereu  10382  nqereq  10388  ltsonq  10422  prlem934  10486  reclem3pr  10502  1re  10672  axsup  10747  addid2  10854  recex  11303  lemul1a  11525  lt2msq  11556  fimaxre2  11616  zdiv  12084  zextlt  12088  prime  12095  uzind2  12107  fzind  12112  lbzbi  12369  qbtwnxr  12627  qextltlem  12629  xralrple  12632  xltneg  12644  xlt2add  12687  supxrgtmnf  12756  ixxub  12793  ixxlb  12794  ioo0  12797  ico0  12818  ioc0  12819  icc0  12820  iocssre  12852  icossre  12853  iccssre  12854  fzen  12966  expclzlem  13496  expaddz  13516  expmulz  13518  hashgadd  13781  hashunsngx  13797  hashgt23el  13828  elovmpowrd  13950  pfxnd0  14090  ccatopth2  14119  pfxccatin12  14135  cshf1  14212  shftuz  14469  cau3lem  14755  caubnd  14759  climuni  14950  lo1resb  14962  o1resb  14964  o1of2  15010  o1add  15011  o1mul  15012  o1sub  15013  ntrivcvgmul  15299  eflt  15511  moddvds  15659  dvdscmulr  15679  dvdsmulcr  15680  dvdsle  15704  divalglem8  15794  divalgb  15798  ndvdssub  15803  bitsfzo  15827  gcdcllem1  15891  gcdcllem3  15893  dvdsgcd  15936  lcmgcdlem  15995  lcmfeq0b  16019  qredeu  16047  isprm3  16072  prmdvdsexpr  16106  prmexpb  16109  eulerthlem2  16167  fermltl  16169  coprimeprodsq  16193  pythagtrip  16219  pcprendvds  16225  pcpremul  16228  pcdvdsb  16253  pc2dvds  16263  4sqlem12  16340  4sqlem18  16346  vdwlem10  16374  cshwshashlem3  16482  xpsrnbas  16895  ismred  16924  mrieqv2d  16961  iscatd  16995  isfuncd  17187  fthestrcsetc  17459  fthsetcestrc  17474  poslubd  17817  dirtr  17905  mulgaddcom  18311  ghmrn  18431  pmtrprfv3  18642  mndodcongi  18731  oddvdsnn0  18732  oddvds  18735  odcl2  18752  odhash3  18761  gexdvds  18769  pgpfi  18790  lsmss1b  18852  lsmss2b  18854  efgsrel  18920  efgred  18934  cntzcmn  19021  cyggenod  19064  lt6abl  19076  gsumcom2  19156  pgpfac1lem2  19258  pgpfac1lem3  19260  dvdsunit  19477  unitmulclb  19479  irredrmul  19521  isabvd  19652  lmodvsdi  19718  lss0cl  19779  islbs3  19988  lbsextlem2  19992  xrsdsreclblem  20205  psrbaglefi  20687  mvrf1  20746  coe1fzgsumd  21019  gsummoncoe1  21021  evl1gsumd  21069  scmataddcl  21209  scmatsubcl  21210  mdetunilem9  21313  mdetuni0  21314  mdetmul  21316  m2cpmrngiso  21451  pm2mpf1  21492  opnnei  21813  neindisj2  21816  cncls2  21966  cncls  21967  cnntr  21968  cnpresti  21981  cnprest  21982  lmcnp  21997  isreg2  22070  ordthauslem  22076  unconn  22122  2ndc1stc  22144  kgen2ss  22248  ptclsg  22308  cnmptcom  22371  kqfvima  22423  hmeof1o  22457  fbncp  22532  fbfinnfr  22534  trfbas2  22536  isufil2  22601  ufprim  22602  trufil  22603  filufint  22613  hausflim  22674  flimrest  22676  flimcls  22678  cnpfcf  22734  alexsubALT  22744  tmdgsum  22788  opnsubg  22801  cldsubg  22804  qustgpopn  22813  tsmsxp  22848  blpnf  23092  blssps  23119  blss  23120  blssec  23130  neibl  23196  prdsxmslem2  23224  xrsmopn  23506  metnrm  23556  climcncf  23594  iccpnfhmeo  23639  xrhmeo  23640  bndth  23652  cphsqrtcl3  23881  iscau2  23970  iscmet3lem2  23985  bcthlem5  24021  bcth3  24024  ishl2  24063  ivthlem1  24144  cmmbl  24227  iundisj2  24242  voliunlem2  24244  mbfaddlem  24353  itg2itg1  24429  itg2seq  24435  itg2mulclem  24439  cnplimc  24579  dvres2  24604  deg1nn0clb  24783  deg1lt0  24784  deg1ge  24791  plypf1  24901  plyadd  24906  plymul  24907  coeeu  24914  dgrub2  24924  coeidlem  24926  coeid3  24929  coemullem  24939  coe11  24942  coemulhi  24943  coemulc  24944  dgreq0  24954  dgrlt  24955  dgradd2  24957  vieta1lem2  24999  tanord1  25221  tanord  25222  logccne0  25262  cxpeq0  25361  cxpmul2z  25374  cxpcn3lem  25428  relogbzcl  25452  angpieqvd  25509  o1cxp  25652  scvxcvx  25663  chtublem  25887  bposlem3  25962  lgsqr  26027  2sqnn  26115  dchrisumlema  26164  dchrisumlem2  26166  ostth2lem3  26311  tghilberti2  26524  inagswap  26727  f1otrg  26757  brbtwn2  26791  axpasch  26827  axcontlem4  26853  axcontlem5  26854  upgredg2vtx  27026  usgredg2vtxeuALT  27104  sizusglecusg  27345  upgredginwlk  27517  frgrwopreg1  28195  frgrwopreg2  28196  frgrregorufrg  28203  lpni  28355  ipasslem5  28710  htthlem  28792  omlsii  29278  spansni  29432  spansneleq  29445  elspansn4  29448  sumspansn  29524  homco1  29676  homulass  29677  mdsl0  30185  ssdmd1  30188  ssdmd2  30189  cvdmd  30212  chirredlem2  30266  atdmd  30273  atmd2  30275  disjif  30432  iundisj2f  30444  isoun  30551  preiman0  30559  padct  30571  iocinioc2  30617  iundisj2fi  30635  archiabllem1a  30964  archiabllem2a  30967  slmdvsdi  30987  ordtconnlem1  31388  indpi1  31500  measinblem  31700  measres  31702  measdivcstALTV  31705  mbfmco2  31744  orvclteinc  31954  sgn3da  32020  sgnnbi  32024  sgnpbi  32025  bnj605  32400  bnj607  32409  bnj964  32436  bnj1033  32462  bnj1128  32483  bnj1137  32488  bnj1136  32490  bnj1413  32528  bnj60  32555  cusgredgex  32592  subgrwlk  32603  acycgr1v  32620  cvmlift2lem10  32783  msubvrs  33031  frpoins3xp3g  33326  wsuclem  33366  nosepon  33426  noextenddif  33429  nolesgn2o  33432  nogesgn1o  33434  nosepne  33441  nodense  33453  dfrdg4  33795  brcolinear2  33902  brsegle2  33953  nn0prpw  34054  ntruni  34058  clsint2  34060  fnessref  34088  fnemeet2  34098  fnejoin2  34100  limsucncmpi  34176  ee7.2aOLD  34192  bj-idreseq  34850  dissneqlem  35030  isbasisrelowllem1  35045  isbasisrelowllem2  35046  icoreclin  35047  poimirlem9  35339  poimirlem30  35360  poimirlem32  35362  areacirc  35423  filbcmb  35451  mettrifi  35468  heiborlem8  35529  heiborlem10  35531  heibor  35532  riscer  35699  igenval2  35777  lshpcmp  36557  eqlkr  36668  lkrlsp2  36672  lkrshp  36674  cvrnbtwn2  36844  cvlexch3  36901  cvlexch4N  36902  cvlatexchb1  36903  cvlsupr3  36913  exatleN  36973  cvratlem  36990  atcvrj2b  37001  cvrat3  37011  cvrat4  37012  athgt  37025  ps-1  37046  ps-2  37047  3atlem5  37056  3at  37059  llnneat  37083  llnmlplnN  37108  lplnneat  37114  lplnnelln  37115  islpln2a  37117  lplnriaN  37119  lplnribN  37120  lplnexllnN  37133  2llnjaN  37135  lvolnle3at  37151  lvolneatN  37157  lvolnelln  37158  lvolnelpln  37159  islvol2aN  37161  dalem62  37303  pmapglb2N  37340  pmapglb2xN  37341  lncmp  37352  paddasslem14  37402  paddasslem15  37403  pmod2iN  37418  hlmod1i  37425  pclfinclN  37519  osumcllem8N  37532  pexmidlem4N  37542  pl42lem1N  37548  pl42lem4N  37551  lhpexle1  37577  lhpexle2lem  37578  lhpmcvr5N  37596  lhpmcvr6N  37597  ltrneq  37718  trlnidatb  37746  cdleme0ex2N  37793  cdleme27a  37936  cdleme17d3  38065  cdlemeg46gfre  38101  cdleme48gfv1  38105  cdlemeg49lebilem  38108  cdlemf2  38131  cdlemf  38132  cdlemfnid  38133  trlord  38138  cdlemg31c  38268  cdlemg35  38282  trlcone  38297  tendoeq2  38343  cdlemj3  38392  cdlemk26b-3  38474  cdlemk33N  38478  cdleml3N  38547  cdlemn  38781  dih1dimb2  38810  dihord5apre  38831  dihmeetlem1N  38859  dihglblem5apreN  38860  dihglblem2N  38863  dihglblem3N  38864  dihmeetlem13N  38888  dihmeetlem15N  38890  dihatexv  38907  hdmap14lem12  39448  uzindd  39537  lcmineqlem1  39589  metakunt1  39640  metakunt5  39644  frlmfzowrdb  39735  nn0rppwr  39823  nn0expgcd  39825  rtprmirr  39837  oddcomabszz  40251  jm2.19lem4  40299  fiuneneq  40507  idomsubgmo  40508  pwinfi3  40628  gneispa  41199  mnringmulrcld  41302  grumnudlem  41359  binomcxplemnn0  41419  addrcom  41545  int3  41684  suctrALT  41898  suctrALTcf  41994  suctrALT3  41996  chordthmALT  42005  iunconnlem2  42007  stoweidlem26  43027  stoweidlem34  43035  issald  43332  goldbachth  44425  nnsgrp  44797  ply1mulgsumlem1  45153