Theorem 3impa 1125

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3imp 1126 by Wolf Lammen, 20-Jun-2022.)

Hypothesis

Ref	Expression
3impa.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3impa	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impa

Step	Hyp	Ref	Expression
1		df-3an 1103	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3impa.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 220	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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-3an 1103

This theorem is referenced by:  3imp  1126  3adant1  1146  3adant2  1147  ex3  1363  3impdir  1368  syl3an9b  1460  biimp3a  1495  stoic3  1803  rspec3  3291  vtocl3gaf  3553  vtocl3ga  3554  rspc3v  3606  raltpg  4669  rextpg  4670  disjiun  5101  otthg  5468  3optocl  5759  fun2ssres  6582  funtpg  6592  funssfv  6903  f1elima  7262  ot1stg  8000  ot2ndg  8001  smogt  8354  omord2  8552  omword  8555  oeword  8576  omabslem  8636  ecovass  8822  fpmg  8866  findcard  9148  endjudisj  10152  cfsmolem  10254  ingru  10800  addasspi  10880  mulasspi  10882  ltapi  10888  ltmpi  10889  axpre-ltadd  11152  leltne  11299  dedekind  11373  recextlem2  11845  divdiv32  11923  divdiv1  11926  lble  12167  fnn0ind  12695  supminf  12959  xrleltne  13170  xrmaxeq  13205  xrmineq  13206  iccgelb  13429  elicc4  13440  iccsplit  13512  elfz  13541  modabs  13937  expgt0  14131  expge0  14134  expge1  14135  mulexpz  14138  expp1z  14147  expm1  14148  expmordi  14203  digit1  14273  faclbnd4  14333  faclbnd5  14334  ccatsymb  14620  s3eqs2s1eq  14975  abssubne0  15368  binom  15884  dvds0lem  16324  dvdsnegb  16331  muldvds1  16338  muldvds2  16339  dvdscmulr  16342  dvdsmulcr  16343  divalgmodcl  16465  gcd2n0cl  16567  gcdaddm  16583  lcmdvds  16666  prmdvdsexp  16774  rpexp1i  16782  monpropd  17794  prfval  18255  xpcpropd  18264  curf2ndf  18303  eqglact  19247  ghmqusker  19357  mndodcongi  19613  oddvdsnn0  19614  efgi0  19790  efgi1  19791  efgsval2  19803  lss0cl  21046  mpofrlmd  21896  evls1fpws  22498  scmatscmid  22632  pmatcollpw3fi1lem1  22912  cnpval  23362  cnf2  23375  cnnei  23408  lfinun  23651  ptpjcn  23737  cnmptk2  23812  flfval  24116  cnmpt2plusg  24214  cnmpt2vsca  24321  ustincl  24334  xbln0  24540  blssec  24561  blpnfctr  24562  mopni2  24619  mopni3  24620  nmoval  24841  nmocl  24846  isnghm2  24850  isnmhm2  24878  cnmpt2ds  24970  metdseq0  24981  cnmpt2ip  25376  caucfil  25411  mbfimasn  25760  dvnf  26055  dvnbss  26056  coemul  26378  dvply1  26414  dvnply2  26417  pserdvlem2  26557  logeftb  26714  advlogexp  26786  cxpne0  26808  cxpp1  26811  elno2  27784  f1otrg  29161  ax5seglem9  29228  uhgrn0  29358  upgrn0  29380  upgrle  29381  uhgrwkspthlem2  30044  frgrhash2wsp  30624  sspval  31016  sspnval  31030  lnof  31048  nmooval  31056  nmooge0  31060  nmoub3i  31066  bloln  31077  nmblore  31079  hosval  32033  homval  32034  hodval  32035  hfsval  32036  hfmval  32037  homulass  32095  hoadddir  32097  nmopub2tALT  32202  nmfnleub2  32219  kbval  32247  lnopmul  32260  0lnfn  32278  lnopcoi  32296  nmcoplb  32323  nmcfnlb  32347  kbass2  32410  nmopleid  32432  hstoh  32525  mdi  32588  dmdi  32595  dmdi4  32600  tpssg  32824  fdifsuppconst  32975  supxrnemnf  33054  elrgspnlem2  33504  rloccring  33532  reofld  33606  nsgmgclem  33664  rhmimaidl  33684  dfufd2lem  33784  r1plmhm  33844  r1pquslmic  33845  lbsdiflsp0  33961  evls1fldgencl  34005  zarclsun  34205  zarclsint  34207  bnj605  35240  bnj607  35249  bnj1097  35314  fnrelpredd  35425  rankfilimb  35439  cusgredgex  35547  topdifinffinlem  37915  lindsdom  38187  lindsenlbs  38188  ftc1anclem2  38267  fzmul  38314  nninfnub  38324  exidreslem  38450  grposnOLD  38455  ghomf  38463  rngohomf  38539  rngohom1  38541  rngohomadd  38542  rngohommul  38543  rngoiso1o  38552  rngoisohom  38553  igenmin  38637  lkrcl  39790  lkrf0  39791  omlfh1N  39956  tendoex  41673  uzindd  42669  primrootsunit1  42788  sticksstones3  42839  sticksstones10  42846  sticksstones12a  42848  sticksstones12  42849  sticksstones17  42854  3anrabdioph  43439  3orrabdioph  43440  rencldnfilem  43473  dvdsabsmod0  43640  jm2.18  43641  jm2.25  43652  jm2.15nn0  43656  tfsconcatlem  43989  onsucunitp  44026  addrfv  45103  subrfv  45104  mulvfv  45105  bi3impa  45120  ssfiunibd  45954  supminfxr  46104  limsupgtlem  46417  xlimmnfv  46474  xlimpnfv  46478  dvnmul  46583  stoweidlem34  46674  stoweidlem48  46688  sge0cl  47021  sge0xp  47069  ovnsubaddlem1  47210  aovmpt4g  47861  gboge9  48452