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  1448  3gencl  3463  moi  3648  disji  5053  disjord  5058  3optocl  5673  sossfld  6078  f1oresrab  6981  soisores  7178  isomin  7188  isofrlem  7191  ovmpos  7399  ov2gf  7400  ndmovord  7440  nnsuc  7705  poxp  7940  brtpos  8022  dfsmo2  8149  smoiun  8163  smoord  8167  smogt  8169  omeulem1  8375  omeu  8378  oewordi  8384  uniinqs  8544  mapvalg  8583  pmvalg  8584  elmapg  8586  xpdom3  8810  mapdom3  8885  php3  8899  unxpdomlem3  8958  isinf  8965  findcard2OLD  8986  isfinite2  9002  ordiso  9205  cnfcom3clem  9393  r111  9464  tskwe  9639  pr2ne  9692  infxpenlem  9700  dfac8alem  9716  infdif  9896  infdif2  9897  cff1  9945  coflim  9948  cfslbn  9954  cfslb2n  9955  cofsmo  9956  cfsmolem  9957  cfcoflem  9959  fin23lem27  10015  isf32lem9  10048  isf34lem6  10067  axcc2lem  10123  domtriomlem  10129  axdc4lem  10142  zorn2lem2  10184  axdclem2  10207  konigthlem  10255  gchen1  10312  gchen2  10313  gchpwdom  10357  gchaleph  10358  winainflem  10380  tskcard  10468  gruiun  10486  gruen  10499  intgru  10501  grudomon  10504  grur1a  10506  grutsk1  10508  nqereu  10616  nqereq  10622  ltsonq  10656  prlem934  10720  reclem3pr  10736  1re  10906  axsup  10981  addid2  11088  recex  11537  lemul1a  11759  lt2msq  11790  fimaxre2  11850  zdiv  12320  zextlt  12324  prime  12331  uzind2  12343  fzind  12348  lbzbi  12605  qbtwnxr  12863  qextltlem  12865  xralrple  12868  xltneg  12880  xlt2add  12923  supxrgtmnf  12992  ixxub  13029  ixxlb  13030  ioo0  13033  ico0  13054  ioc0  13055  icc0  13056  iocssre  13088  icossre  13089  iccssre  13090  fzen  13202  expclzlem  13734  expaddz  13755  expmulz  13757  hashgadd  14020  hashunsngx  14036  hashgt23el  14067  elovmpowrd  14189  pfxnd0  14329  ccatopth2  14358  pfxccatin12  14374  cshf1  14451  shftuz  14708  cau3lem  14994  caubnd  14998  climuni  15189  lo1resb  15201  o1resb  15203  o1of2  15250  o1add  15251  o1mul  15252  o1sub  15253  ntrivcvgmul  15542  eflt  15754  moddvds  15902  dvdscmulr  15922  dvdsmulcr  15923  dvdsle  15947  divalglem8  16037  divalgb  16041  ndvdssub  16046  bitsfzo  16070  gcdcllem1  16134  gcdcllem3  16136  dvdsgcd  16180  lcmgcdlem  16239  lcmfeq0b  16263  qredeu  16291  isprm3  16316  prmdvdsexpr  16350  prmexpb  16353  eulerthlem2  16411  fermltl  16413  coprimeprodsq  16437  pythagtrip  16463  pcprendvds  16469  pcpremul  16472  pcdvdsb  16498  pc2dvds  16508  4sqlem12  16585  4sqlem18  16591  vdwlem10  16619  cshwshashlem3  16727  xpsrnbas  17199  ismred  17228  mrieqv2d  17265  iscatd  17299  isfuncd  17496  fthestrcsetc  17783  fthsetcestrc  17798  poslubd  18046  dirtr  18235  mulgaddcom  18642  ghmrn  18762  pmtrprfv3  18977  mndodcongi  19066  oddvdsnn0  19067  oddvds  19070  odcl2  19087  odhash3  19096  gexdvds  19104  pgpfi  19125  lsmss1b  19187  lsmss2b  19189  efgsrel  19255  efgred  19269  cntzcmn  19356  cyggenod  19399  lt6abl  19411  gsumcom2  19491  pgpfac1lem2  19593  pgpfac1lem3  19595  dvdsunit  19820  unitmulclb  19822  irredrmul  19864  isabvd  19995  lmodvsdi  20061  lss0cl  20123  islbs3  20332  lbsextlem2  20336  xrsdsreclblem  20556  psrbaglefi  21045  mvrf1  21104  coe1fzgsumd  21383  gsummoncoe1  21385  evl1gsumd  21433  scmataddcl  21573  scmatsubcl  21574  mdetunilem9  21677  mdetuni0  21678  mdetmul  21680  m2cpmrngiso  21815  pm2mpf1  21856  opnnei  22179  neindisj2  22182  cncls2  22332  cncls  22333  cnntr  22334  cnpresti  22347  cnprest  22348  lmcnp  22363  isreg2  22436  ordthauslem  22442  unconn  22488  2ndc1stc  22510  kgen2ss  22614  ptclsg  22674  cnmptcom  22737  kqfvima  22789  hmeof1o  22823  fbncp  22898  fbfinnfr  22900  trfbas2  22902  isufil2  22967  ufprim  22968  trufil  22969  filufint  22979  hausflim  23040  flimrest  23042  flimcls  23044  cnpfcf  23100  alexsubALT  23110  tmdgsum  23154  opnsubg  23167  cldsubg  23170  qustgpopn  23179  tsmsxp  23214  blpnf  23458  blssps  23485  blss  23486  blssec  23496  neibl  23563  prdsxmslem2  23591  xrsmopn  23881  metnrm  23931  climcncf  23969  iccpnfhmeo  24014  xrhmeo  24015  bndth  24027  cphsqrtcl3  24256  iscau2  24346  iscmet3lem2  24361  bcthlem5  24397  bcth3  24400  ishl2  24439  ivthlem1  24520  cmmbl  24603  iundisj2  24618  voliunlem2  24620  mbfaddlem  24729  itg2itg1  24806  itg2seq  24812  itg2mulclem  24816  cnplimc  24956  dvres2  24981  deg1nn0clb  25160  deg1lt0  25161  deg1ge  25168  plypf1  25278  plyadd  25283  plymul  25284  coeeu  25291  dgrub2  25301  coeidlem  25303  coeid3  25306  coemullem  25316  coe11  25319  coemulhi  25320  coemulc  25321  dgreq0  25331  dgrlt  25332  dgradd2  25334  vieta1lem2  25376  tanord1  25598  tanord  25599  logccne0  25639  cxpeq0  25738  cxpmul2z  25751  cxpcn3lem  25805  relogbzcl  25829  angpieqvd  25886  o1cxp  26029  scvxcvx  26040  chtublem  26264  bposlem3  26339  lgsqr  26404  2sqnn  26492  dchrisumlema  26541  dchrisumlem2  26543  ostth2lem3  26688  tghilberti2  26903  inagswap  27106  f1otrg  27136  brbtwn2  27176  axpasch  27212  axcontlem4  27238  axcontlem5  27239  upgredg2vtx  27414  usgredg2vtxeuALT  27492  sizusglecusg  27733  upgredginwlk  27905  frgrwopreg1  28583  frgrwopreg2  28584  frgrregorufrg  28591  lpni  28743  ipasslem5  29098  htthlem  29180  omlsii  29666  spansni  29820  spansneleq  29833  elspansn4  29836  sumspansn  29912  homco1  30064  homulass  30065  mdsl0  30573  ssdmd1  30576  ssdmd2  30577  cvdmd  30600  chirredlem2  30654  atdmd  30661  atmd2  30663  disjif  30818  iundisj2f  30830  isoun  30936  preiman0  30944  padct  30956  iocinioc2  31002  iundisj2fi  31020  archiabllem1a  31347  archiabllem2a  31350  slmdvsdi  31370  ordtconnlem1  31776  indpi1  31888  measinblem  32088  measres  32090  measdivcstALTV  32093  mbfmco2  32132  orvclteinc  32342  sgn3da  32408  sgnnbi  32412  sgnpbi  32413  bnj605  32787  bnj607  32796  bnj964  32823  bnj1033  32849  bnj1128  32870  bnj1137  32875  bnj1136  32877  bnj1413  32915  bnj60  32942  fineqvac  32966  cusgredgex  32983  subgrwlk  32994  acycgr1v  33011  cvmlift2lem10  33174  msubvrs  33422  frpoins3xp3g  33715  wsuclem  33746  nosepon  33795  noextenddif  33798  nolesgn2o  33801  nogesgn1o  33803  nosepne  33810  nodense  33822  dfrdg4  34180  brcolinear2  34287  brsegle2  34338  nn0prpw  34439  ntruni  34443  clsint2  34445  fnessref  34473  fnemeet2  34483  fnejoin2  34485  limsucncmpi  34561  ee7.2aOLD  34577  bj-idreseq  35260  dissneqlem  35438  isbasisrelowllem1  35453  isbasisrelowllem2  35454  icoreclin  35455  poimirlem9  35713  poimirlem30  35734  poimirlem32  35736  areacirc  35797  filbcmb  35825  mettrifi  35842  heiborlem8  35903  heiborlem10  35905  heibor  35906  riscer  36073  igenval2  36151  lshpcmp  36929  eqlkr  37040  lkrlsp2  37044  lkrshp  37046  cvrnbtwn2  37216  cvlexch3  37273  cvlexch4N  37274  cvlatexchb1  37275  cvlsupr3  37285  exatleN  37345  cvratlem  37362  atcvrj2b  37373  cvrat3  37383  cvrat4  37384  athgt  37397  ps-1  37418  ps-2  37419  3atlem5  37428  3at  37431  llnneat  37455  llnmlplnN  37480  lplnneat  37486  lplnnelln  37487  islpln2a  37489  lplnriaN  37491  lplnribN  37492  lplnexllnN  37505  2llnjaN  37507  lvolnle3at  37523  lvolneatN  37529  lvolnelln  37530  lvolnelpln  37531  islvol2aN  37533  dalem62  37675  pmapglb2N  37712  pmapglb2xN  37713  lncmp  37724  paddasslem14  37774  paddasslem15  37775  pmod2iN  37790  hlmod1i  37797  pclfinclN  37891  osumcllem8N  37904  pexmidlem4N  37914  pl42lem1N  37920  pl42lem4N  37923  lhpexle1  37949  lhpexle2lem  37950  lhpmcvr5N  37968  lhpmcvr6N  37969  ltrneq  38090  trlnidatb  38118  cdleme0ex2N  38165  cdleme27a  38308  cdleme17d3  38437  cdlemeg46gfre  38473  cdleme48gfv1  38477  cdlemeg49lebilem  38480  cdlemf2  38503  cdlemf  38504  cdlemfnid  38505  trlord  38510  cdlemg31c  38640  cdlemg35  38654  trlcone  38669  tendoeq2  38715  cdlemj3  38764  cdlemk26b-3  38846  cdlemk33N  38850  cdleml3N  38919  cdlemn  39153  dih1dimb2  39182  dihord5apre  39203  dihmeetlem1N  39231  dihglblem5apreN  39232  dihglblem2N  39235  dihglblem3N  39236  dihmeetlem13N  39260  dihmeetlem15N  39262  dihatexv  39279  hdmap14lem12  39820  uzindd  39913  lcmineqlem1  39965  sticksstones1  40030  metakunt1  40053  metakunt5  40057  frlmfzowrdb  40161  nn0rppwr  40254  nn0expgcd  40256  dvdsexpnn0  40262  rtprmirr  40268  oddcomabszz  40682  jm2.19lem4  40730  fiuneneq  40938  idomsubgmo  40939  pwinfi3  41059  gneispa  41629  mnringmulrcld  41735  grumnudlem  41792  ismnushort  41808  binomcxplemnn0  41856  addrcom  41982  int3  42121  suctrALT  42335  suctrALTcf  42431  suctrALT3  42433  chordthmALT  42442  iunconnlem2  42444  stoweidlem26  43457  stoweidlem34  43465  issald  43762  goldbachth  44887  nnsgrp  45259  ply1mulgsumlem1  45615  lubsscl  46142  glbsscl  46143