Theorem 3expia 1122

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

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

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 1089

This theorem is referenced by:  ad5ant125  1369  mp3an3  1453  3gencl  3474  vtocl3gaf  3525  vtocl3ga  3527  moi  3665  disji  5071  disjord  5075  3optocl  5721  sossfld  6144  f1oresrab  7074  f1cdmsn  7230  soisores  7275  isomin  7285  isofrlem  7288  ovmpos  7508  ov2gf  7509  ndmovord  7550  nnsuc  7828  poxp  8071  frpoins3xp3g  8084  brtpos  8178  dfsmo2  8280  smoiun  8294  smoord  8298  smogt  8300  omeulem1  8510  omeu  8513  oewordi  8520  uniinqs  8737  mapvalg  8776  pmvalg  8777  elmapg  8779  xpdom3  9006  mapdom3  9080  sdomdomtrfi  9128  domsdomtrfi  9129  php  9134  php3  9136  nndomog  9140  onomeneq  9141  sucdom  9147  unxpdomlem3  9161  isinf  9168  f1finf1o  9176  isfinite2  9201  prfi  9227  ordiso  9424  cnfcom3clem  9617  r111  9690  tskwe  9865  pr2ne  9918  infxpenlem  9926  dfac8alem  9942  infdif  10121  infdif2  10122  cff1  10171  coflim  10174  cfslbn  10180  cfslb2n  10181  cofsmo  10182  cfsmolem  10183  cfcoflem  10185  fin23lem27  10241  isf32lem9  10274  isf34lem6  10293  axcc2lem  10349  domtriomlem  10355  axdc4lem  10368  zorn2lem2  10410  axdclem2  10433  konigthlem  10482  gchen1  10539  gchen2  10540  gchpwdom  10584  gchaleph  10585  winainflem  10607  tskcard  10695  gruiun  10713  gruen  10726  intgru  10728  grudomon  10731  grur1a  10733  grutsk1  10735  nqereu  10843  nqereq  10849  ltsonq  10883  prlem934  10947  reclem3pr  10963  1re  11135  axsup  11212  addlid  11320  recex  11773  lemul1a  12000  lt2msq  12032  fimaxre2  12092  indpi1  12164  zdiv  12590  zextlt  12594  prime  12601  uzind2  12613  fzind  12618  lbzbi  12877  qbtwnxr  13143  qextltlem  13145  xralrple  13148  xltneg  13160  xlt2add  13203  supxrgtmnf  13272  ixxub  13310  ixxlb  13311  ioo0  13314  ico0  13335  ioc0  13336  icc0  13337  iocssre  13371  icossre  13372  iccssre  13373  fzen  13486  expclzlem  14036  expaddz  14059  expmulz  14061  hashgadd  14330  hashunsngx  14346  hashgt23el  14377  elovmpowrd  14511  pfxnd0  14642  ccatopth2  14670  pfxccatin12  14686  cshf1  14763  shftuz  15022  cau3lem  15308  caubnd  15312  climuni  15505  lo1resb  15517  o1resb  15519  o1of2  15566  o1add  15567  o1mul  15568  o1sub  15569  ntrivcvgmul  15858  eflt  16075  moddvds  16223  dvdscmulr  16244  dvdsmulcr  16245  dvdsle  16270  divalglem8  16360  divalgb  16364  ndvdssub  16369  bitsfzo  16395  gcdcllem1  16459  gcdcllem3  16461  dvdsgcd  16504  nn0rppwr  16521  nn0expgcd  16524  lcmgcdlem  16566  lcmfeq0b  16590  qredeu  16618  isprm3  16643  prmdvdsexpr  16678  prmexpb  16680  eulerthlem2  16743  fermltl  16745  coprimeprodsq  16770  pythagtrip  16796  pcprendvds  16802  pcpremul  16805  pcdvdsb  16831  pc2dvds  16841  4sqlem12  16918  4sqlem18  16924  vdwlem10  16952  cshwshashlem3  17059  xpsrnbas  17526  ismred  17555  mrieqv2d  17596  iscatd  17630  isfuncd  17823  fthestrcsetc  18107  fthsetcestrc  18122  poslubd  18368  dirtr  18559  mulgaddcom  19065  ghmrn  19195  pmtrprfv3  19420  mndodcongi  19509  oddvdsnn0  19510  oddvds  19513  odcl2  19531  odhash3  19542  gexdvds  19550  pgpfi  19571  lsmss1b  19632  lsmss2b  19634  efgsrel  19700  efgred  19714  cntzcmn  19806  cyggenod  19850  lt6abl  19861  gsumcom2  19941  pgpfac1lem2  20043  pgpfac1lem3  20045  dvdsunit  20350  unitmulclb  20352  irredrmul  20398  isabvd  20780  lmodvsdi  20871  lss0cl  20933  islbs3  21145  lbsextlem2  21149  xrsdsreclblem  21402  psrbaglefi  21916  mvrf1  21974  coe1fzgsumd  22279  gsummoncoe1  22283  evl1gsumd  22332  scmataddcl  22491  scmatsubcl  22492  mdetunilem9  22595  mdetuni0  22596  mdetmul  22598  m2cpmrngiso  22733  pm2mpf1  22774  opnnei  23095  neindisj2  23098  cncls2  23248  cncls  23249  cnntr  23250  cnpresti  23263  cnprest  23264  lmcnp  23279  isreg2  23352  ordthauslem  23358  unconn  23404  2ndc1stc  23426  kgen2ss  23530  ptclsg  23590  cnmptcom  23653  kqfvima  23705  hmeof1o  23739  fbncp  23814  fbfinnfr  23816  trfbas2  23818  isufil2  23883  ufprim  23884  trufil  23885  filufint  23895  hausflim  23956  flimrest  23958  flimcls  23960  cnpfcf  24016  alexsubALT  24026  tmdgsum  24070  opnsubg  24083  cldsubg  24086  qustgpopn  24095  tsmsxp  24130  blpnf  24372  blssps  24399  blss  24400  blssec  24410  neibl  24476  prdsxmslem2  24504  xrsmopn  24788  metnrm  24838  climcncf  24877  iccpnfhmeo  24922  xrhmeo  24923  bndth  24935  cphsqrtcl3  25164  iscau2  25254  iscmet3lem2  25269  bcthlem5  25305  bcth3  25308  ishl2  25347  ivthlem1  25428  cmmbl  25511  iundisj2  25526  voliunlem2  25528  mbfaddlem  25637  itg2itg1  25713  itg2seq  25719  itg2mulclem  25723  cnplimc  25864  dvres2  25889  deg1nn0clb  26065  deg1lt0  26066  deg1ge  26073  plypf1  26187  plyadd  26192  plymul  26193  coeeu  26200  dgrub2  26210  coeidlem  26212  coeid3  26215  coemullem  26225  coe11  26228  coemulhi  26229  coemulc  26230  dgreq0  26240  dgrlt  26241  dgradd2  26243  vieta1lem2  26288  tanord1  26514  tanord  26515  logccne0  26555  cxpeq0  26655  cxpmul2z  26668  cxpcn3lem  26724  rtprmirr  26737  relogbzcl  26751  angpieqvd  26808  o1cxp  26952  scvxcvx  26963  chtublem  27188  bposlem3  27263  lgsqr  27328  2sqnn  27416  dchrisumlema  27465  dchrisumlem2  27467  ostth2lem3  27612  nosepon  27643  noextenddif  27646  nolesgn2o  27649  nogesgn1o  27651  nosepne  27658  nodense  27670  onnolt  28272  onlts  28273  oniso  28277  bdayn0p1  28375  bdayn0sf1o  28376  tghilberti2  28720  inagswap  28923  f1otrg  28953  brbtwn2  28988  axpasch  29024  axcontlem4  29050  axcontlem5  29051  upgredg2vtx  29224  usgredg2vtxeuALT  29305  sizusglecusg  29547  upgredginwlk  29719  frgrwopreg1  30403  frgrwopreg2  30404  frgrregorufrg  30411  lpni  30566  ipasslem5  30921  htthlem  31003  omlsii  31489  spansni  31643  spansneleq  31656  elspansn4  31659  sumspansn  31735  homco1  31887  homulass  31888  mdsl0  32396  ssdmd1  32399  ssdmd2  32400  cvdmd  32423  chirredlem2  32477  atdmd  32484  atmd2  32486  disjif  32663  iundisj2f  32675  isoun  32790  preiman0  32798  padct  32806  iocinioc2  32867  iundisj2fi  32885  sgn3da  32922  sgnnbi  32926  sgnpbi  32927  archiabllem1a  33267  archiabllem2a  33270  slmdvsdi  33291  ordtconnlem1  34084  measinblem  34380  measres  34382  measdivcstALTV  34385  mbfmco2  34425  orvclteinc  34636  bnj605  35065  bnj607  35074  bnj964  35101  bnj1033  35127  bnj1128  35148  bnj1137  35153  bnj1136  35155  bnj1413  35193  bnj60  35220  rankfilimb  35261  r1filim  35263  fineqvac  35276  fineqvnttrclselem3  35283  fineqvnttrclse  35284  cusgredgex  35320  subgrwlk  35330  acycgr1v  35347  cvmlift2lem10  35510  msubvrs  35758  wsuclem  36021  dfrdg4  36149  brcolinear2  36256  brsegle2  36307  nn0prpw  36521  ntruni  36525  clsint2  36527  fnessref  36555  fnemeet2  36565  fnejoin2  36567  limsucncmpi  36643  ee7.2aOLD  36659  bj-idreseq  37492  dissneqlem  37670  isbasisrelowllem1  37685  isbasisrelowllem2  37686  icoreclin  37687  poimirlem9  37964  poimirlem30  37985  poimirlem32  37987  areacirc  38048  filbcmb  38075  mettrifi  38092  heiborlem8  38153  heiborlem10  38155  heibor  38156  riscer  38323  igenval2  38401  eldisjim3  39150  eldisjs6  39275  lshpcmp  39448  eqlkr  39559  lkrlsp2  39563  lkrshp  39565  cvrnbtwn2  39735  cvlexch3  39792  cvlexch4N  39793  cvlatexchb1  39794  cvlsupr3  39804  exatleN  39864  cvratlem  39881  atcvrj2b  39892  cvrat3  39902  cvrat4  39903  athgt  39916  ps-1  39937  ps-2  39938  3atlem5  39947  3at  39950  llnneat  39974  llnmlplnN  39999  lplnneat  40005  lplnnelln  40006  islpln2a  40008  lplnriaN  40010  lplnribN  40011  lplnexllnN  40024  2llnjaN  40026  lvolnle3at  40042  lvolneatN  40048  lvolnelln  40049  lvolnelpln  40050  islvol2aN  40052  dalem62  40194  pmapglb2N  40231  pmapglb2xN  40232  lncmp  40243  paddasslem14  40293  paddasslem15  40294  pmod2iN  40309  hlmod1i  40316  pclfinclN  40410  osumcllem8N  40423  pexmidlem4N  40433  pl42lem1N  40439  pl42lem4N  40442  lhpexle1  40468  lhpexle2lem  40469  lhpmcvr5N  40487  lhpmcvr6N  40488  ltrneq  40609  trlnidatb  40637  cdleme0ex2N  40684  cdleme27a  40827  cdleme17d3  40956  cdlemeg46gfre  40992  cdleme48gfv1  40996  cdlemeg49lebilem  40999  cdlemf2  41022  cdlemf  41023  cdlemfnid  41024  trlord  41029  cdlemg31c  41159  cdlemg35  41173  trlcone  41188  tendoeq2  41234  cdlemj3  41283  cdlemk26b-3  41365  cdlemk33N  41369  cdleml3N  41438  cdlemn  41672  dih1dimb2  41701  dihord5apre  41722  dihmeetlem1N  41750  dihglblem5apreN  41751  dihglblem2N  41754  dihglblem3N  41755  dihmeetlem13N  41779  dihmeetlem15N  41781  dihatexv  41798  hdmap14lem12  42339  uzindd  42431  lcmineqlem1  42482  sticksstones1  42599  dvdsexpnn0  42780  frlmfzowrdb  42963  oddcomabszz  43390  jm2.19lem4  43438  fiuneneq  43638  idomsubgmo  43639  omcl2  43779  pwinfi3  44008  gneispa  44575  mnringmulrcld  44673  grumnudlem  44730  ismnushort  44746  binomcxplemnn0  44794  addrcom  44919  int3  45057  suctrALT  45270  suctrALTcf  45366  suctrALT3  45368  chordthmALT  45377  iunconnlem2  45379  relpmin  45397  relpfrlem  45398  stoweidlem26  46472  stoweidlem34  46480  issald  46779  goldbachth  48022  nprmdvdsfacm1  48099  grlimgrtri  48491  nnsgrp  48665  ply1mulgsumlem1  48874  lubsscl  49447  glbsscl  49448