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

This theorem is referenced by:  ad5ant125  1365  mp3an3  1449  3gencl  3517  moi  3714  disji  5131  disjord  5136  3optocl  5772  sossfld  6185  f1oresrab  7127  f1cdmsn  7283  soisores  7327  isomin  7337  isofrlem  7340  ovmpos  7559  ov2gf  7560  ndmovord  7601  nnsuc  7877  poxp  8118  frpoins3xp3g  8131  brtpos  8224  dfsmo2  8351  smoiun  8365  smoord  8369  smogt  8371  omeulem1  8586  omeu  8589  oewordi  8595  uniinqs  8795  mapvalg  8834  pmvalg  8835  elmapg  8837  xpdom3  9074  mapdom3  9153  sdomdomtrfi  9208  domsdomtrfi  9209  php  9214  php3  9216  nndomog  9220  php3OLD  9228  onomeneq  9232  sucdom  9239  unxpdomlem3  9256  isinf  9264  isinfOLD  9265  f1finf1o  9275  findcard2OLD  9288  isfinite2  9305  ordiso  9515  cnfcom3clem  9704  r111  9774  tskwe  9949  pr2ne  10003  pr2neOLD  10004  infxpenlem  10012  dfac8alem  10028  infdif  10208  infdif2  10209  cff1  10257  coflim  10260  cfslbn  10266  cfslb2n  10267  cofsmo  10268  cfsmolem  10269  cfcoflem  10271  fin23lem27  10327  isf32lem9  10360  isf34lem6  10379  axcc2lem  10435  domtriomlem  10441  axdc4lem  10454  zorn2lem2  10496  axdclem2  10519  konigthlem  10567  gchen1  10624  gchen2  10625  gchpwdom  10669  gchaleph  10670  winainflem  10692  tskcard  10780  gruiun  10798  gruen  10811  intgru  10813  grudomon  10816  grur1a  10818  grutsk1  10820  nqereu  10928  nqereq  10934  ltsonq  10968  prlem934  11032  reclem3pr  11048  1re  11219  axsup  11294  addlid  11402  recex  11851  lemul1a  12073  lt2msq  12104  fimaxre2  12164  zdiv  12637  zextlt  12641  prime  12648  uzind2  12660  fzind  12665  lbzbi  12925  qbtwnxr  13184  qextltlem  13186  xralrple  13189  xltneg  13201  xlt2add  13244  supxrgtmnf  13313  ixxub  13350  ixxlb  13351  ioo0  13354  ico0  13375  ioc0  13376  icc0  13377  iocssre  13409  icossre  13410  iccssre  13411  fzen  13523  expclzlem  14054  expaddz  14077  expmulz  14079  hashgadd  14342  hashunsngx  14358  hashgt23el  14389  elovmpowrd  14513  pfxnd0  14643  ccatopth2  14672  pfxccatin12  14688  cshf1  14765  shftuz  15021  cau3lem  15306  caubnd  15310  climuni  15501  lo1resb  15513  o1resb  15515  o1of2  15562  o1add  15563  o1mul  15564  o1sub  15565  ntrivcvgmul  15853  eflt  16065  moddvds  16213  dvdscmulr  16233  dvdsmulcr  16234  dvdsle  16258  divalglem8  16348  divalgb  16352  ndvdssub  16357  bitsfzo  16381  gcdcllem1  16445  gcdcllem3  16447  dvdsgcd  16491  lcmgcdlem  16548  lcmfeq0b  16572  qredeu  16600  isprm3  16625  prmdvdsexpr  16659  prmexpb  16662  eulerthlem2  16720  fermltl  16722  coprimeprodsq  16746  pythagtrip  16772  pcprendvds  16778  pcpremul  16781  pcdvdsb  16807  pc2dvds  16817  4sqlem12  16894  4sqlem18  16900  vdwlem10  16928  cshwshashlem3  17036  xpsrnbas  17522  ismred  17551  mrieqv2d  17588  iscatd  17622  isfuncd  17820  fthestrcsetc  18107  fthsetcestrc  18122  poslubd  18371  dirtr  18560  mulgaddcom  19015  ghmrn  19144  pmtrprfv3  19364  mndodcongi  19453  oddvdsnn0  19454  oddvds  19457  odcl2  19475  odhash3  19486  gexdvds  19494  pgpfi  19515  lsmss1b  19576  lsmss2b  19578  efgsrel  19644  efgred  19658  cntzcmn  19750  cyggenod  19794  lt6abl  19805  gsumcom2  19885  pgpfac1lem2  19987  pgpfac1lem3  19989  dvdsunit  20271  unitmulclb  20273  irredrmul  20319  isabvd  20572  lmodvsdi  20640  lss0cl  20702  islbs3  20914  lbsextlem2  20918  xrsdsreclblem  21192  psrbaglefi  21705  mvrf1  21765  coe1fzgsumd  22047  gsummoncoe1  22049  evl1gsumd  22097  scmataddcl  22239  scmatsubcl  22240  mdetunilem9  22343  mdetuni0  22344  mdetmul  22346  m2cpmrngiso  22481  pm2mpf1  22522  opnnei  22845  neindisj2  22848  cncls2  22998  cncls  22999  cnntr  23000  cnpresti  23013  cnprest  23014  lmcnp  23029  isreg2  23102  ordthauslem  23108  unconn  23154  2ndc1stc  23176  kgen2ss  23280  ptclsg  23340  cnmptcom  23403  kqfvima  23455  hmeof1o  23489  fbncp  23564  fbfinnfr  23566  trfbas2  23568  isufil2  23633  ufprim  23634  trufil  23635  filufint  23645  hausflim  23706  flimrest  23708  flimcls  23710  cnpfcf  23766  alexsubALT  23776  tmdgsum  23820  opnsubg  23833  cldsubg  23836  qustgpopn  23845  tsmsxp  23880  blpnf  24124  blssps  24151  blss  24152  blssec  24162  neibl  24231  prdsxmslem2  24259  xrsmopn  24549  metnrm  24599  climcncf  24641  iccpnfhmeo  24691  xrhmeo  24692  bndth  24705  cphsqrtcl3  24936  iscau2  25026  iscmet3lem2  25041  bcthlem5  25077  bcth3  25080  ishl2  25119  ivthlem1  25201  cmmbl  25284  iundisj2  25299  voliunlem2  25301  mbfaddlem  25410  itg2itg1  25487  itg2seq  25493  itg2mulclem  25497  cnplimc  25637  dvres2  25662  deg1nn0clb  25844  deg1lt0  25845  deg1ge  25852  plypf1  25962  plyadd  25967  plymul  25968  coeeu  25975  dgrub2  25985  coeidlem  25987  coeid3  25990  coemullem  26000  coe11  26003  coemulhi  26004  coemulc  26005  dgreq0  26016  dgrlt  26017  dgradd2  26019  vieta1lem2  26061  tanord1  26283  tanord  26284  logccne0  26324  cxpeq0  26423  cxpmul2z  26436  cxpcn3lem  26492  relogbzcl  26516  angpieqvd  26573  o1cxp  26716  scvxcvx  26727  chtublem  26951  bposlem3  27026  lgsqr  27091  2sqnn  27179  dchrisumlema  27228  dchrisumlem2  27230  ostth2lem3  27375  nosepon  27405  noextenddif  27408  nolesgn2o  27411  nogesgn1o  27413  nosepne  27420  nodense  27432  tghilberti2  28157  inagswap  28360  f1otrg  28390  brbtwn2  28431  axpasch  28467  axcontlem4  28493  axcontlem5  28494  upgredg2vtx  28669  usgredg2vtxeuALT  28747  sizusglecusg  28988  upgredginwlk  29161  frgrwopreg1  29839  frgrwopreg2  29840  frgrregorufrg  29847  lpni  30001  ipasslem5  30356  htthlem  30438  omlsii  30924  spansni  31078  spansneleq  31091  elspansn4  31094  sumspansn  31170  homco1  31322  homulass  31323  mdsl0  31831  ssdmd1  31834  ssdmd2  31835  cvdmd  31858  chirredlem2  31912  atdmd  31919  atmd2  31921  disjif  32077  iundisj2f  32089  isoun  32191  preiman0  32199  padct  32212  iocinioc2  32258  iundisj2fi  32276  archiabllem1a  32608  archiabllem2a  32611  slmdvsdi  32631  ordtconnlem1  33203  indpi1  33317  measinblem  33517  measres  33519  measdivcstALTV  33522  mbfmco2  33563  orvclteinc  33773  sgn3da  33839  sgnnbi  33843  sgnpbi  33844  bnj605  34217  bnj607  34226  bnj964  34253  bnj1033  34279  bnj1128  34300  bnj1137  34305  bnj1136  34307  bnj1413  34345  bnj60  34372  fineqvac  34396  cusgredgex  34411  subgrwlk  34422  acycgr1v  34439  cvmlift2lem10  34602  msubvrs  34850  wsuclem  35102  dfrdg4  35228  brcolinear2  35335  brsegle2  35386  nn0prpw  35512  ntruni  35516  clsint2  35518  fnessref  35546  fnemeet2  35556  fnejoin2  35558  limsucncmpi  35634  ee7.2aOLD  35650  bj-idreseq  36347  dissneqlem  36525  isbasisrelowllem1  36540  isbasisrelowllem2  36541  icoreclin  36542  poimirlem9  36801  poimirlem30  36822  poimirlem32  36824  areacirc  36885  filbcmb  36912  mettrifi  36929  heiborlem8  36990  heiborlem10  36992  heibor  36993  riscer  37160  igenval2  37238  lshpcmp  38162  eqlkr  38273  lkrlsp2  38277  lkrshp  38279  cvrnbtwn2  38449  cvlexch3  38506  cvlexch4N  38507  cvlatexchb1  38508  cvlsupr3  38518  exatleN  38579  cvratlem  38596  atcvrj2b  38607  cvrat3  38617  cvrat4  38618  athgt  38631  ps-1  38652  ps-2  38653  3atlem5  38662  3at  38665  llnneat  38689  llnmlplnN  38714  lplnneat  38720  lplnnelln  38721  islpln2a  38723  lplnriaN  38725  lplnribN  38726  lplnexllnN  38739  2llnjaN  38741  lvolnle3at  38757  lvolneatN  38763  lvolnelln  38764  lvolnelpln  38765  islvol2aN  38767  dalem62  38909  pmapglb2N  38946  pmapglb2xN  38947  lncmp  38958  paddasslem14  39008  paddasslem15  39009  pmod2iN  39024  hlmod1i  39031  pclfinclN  39125  osumcllem8N  39138  pexmidlem4N  39148  pl42lem1N  39154  pl42lem4N  39157  lhpexle1  39183  lhpexle2lem  39184  lhpmcvr5N  39202  lhpmcvr6N  39203  ltrneq  39324  trlnidatb  39352  cdleme0ex2N  39399  cdleme27a  39542  cdleme17d3  39671  cdlemeg46gfre  39707  cdleme48gfv1  39711  cdlemeg49lebilem  39714  cdlemf2  39737  cdlemf  39738  cdlemfnid  39739  trlord  39744  cdlemg31c  39874  cdlemg35  39888  trlcone  39903  tendoeq2  39949  cdlemj3  39998  cdlemk26b-3  40080  cdlemk33N  40084  cdleml3N  40153  cdlemn  40387  dih1dimb2  40416  dihord5apre  40437  dihmeetlem1N  40465  dihglblem5apreN  40466  dihglblem2N  40469  dihglblem3N  40470  dihmeetlem13N  40494  dihmeetlem15N  40496  dihatexv  40513  hdmap14lem12  41054  uzindd  41149  lcmineqlem1  41201  sticksstones1  41269  metakunt1  41292  metakunt5  41296  frlmfzowrdb  41385  nn0rppwr  41527  nn0expgcd  41529  dvdsexpnn0  41535  rtprmirr  41540  oddcomabszz  41986  jm2.19lem4  42034  fiuneneq  42242  idomsubgmo  42243  omcl2  42386  pwinfi3  42617  gneispa  43184  mnringmulrcld  43290  grumnudlem  43347  ismnushort  43363  binomcxplemnn0  43411  addrcom  43537  int3  43676  suctrALT  43890  suctrALTcf  43986  suctrALT3  43988  chordthmALT  43997  iunconnlem2  43999  stoweidlem26  45041  stoweidlem34  45049  issald  45348  goldbachth  46514  nnsgrp  46854  ply1mulgsumlem1  47155  lubsscl  47681  glbsscl  47682