Theorem 3impa 1109

Description: Importation from double to triple conjunction. (Contributed by NM, 20-Aug-1995.) (Revised to shorten 3imp 1110 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 1088	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		3impa.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylbi 217	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 207  df-3an 1088

This theorem is referenced by:  3imp  1110  3adant1  1130  3adant2  1131  ex3  1347  3impdir  1352  syl3an9b  1436  biimp3a  1471  stoic3  1777  rspec3  3254  vtocl3gaf  3534  vtocl3ga  3536  rspc3v  3590  raltpg  4653  rextpg  4654  disjiun  5084  otthg  5431  3optocl  5719  fun2ssres  6535  funtpg  6545  funssfv  6853  f1elima  7207  ot1stg  7945  ot2ndg  7946  smogt  8297  omord2  8492  omword  8495  oeword  8516  omabslem  8576  ecovass  8759  fpmg  8804  findcard  9086  endjudisj  10077  cfsmolem  10178  ingru  10724  addasspi  10804  mulasspi  10806  ltapi  10812  ltmpi  10813  axpre-ltadd  11076  leltne  11220  dedekind  11294  recextlem2  11766  divdiv32  11847  divdiv1  11850  lble  12092  fnn0ind  12589  supminf  12846  xrleltne  13057  xrmaxeq  13092  xrmineq  13093  iccgelb  13316  elicc4  13327  iccsplit  13399  elfz  13427  modabs  13822  expgt0  14016  expge0  14019  expge1  14020  mulexpz  14023  expp1z  14032  expm1  14033  expmordi  14088  digit1  14158  faclbnd4  14218  faclbnd5  14219  ccatsymb  14504  s3eqs2s1eq  14859  abssubne0  15238  binom  15751  dvds0lem  16191  dvdsnegb  16198  muldvds1  16205  muldvds2  16206  dvdscmulr  16209  dvdsmulcr  16210  divalgmodcl  16332  gcd2n0cl  16434  gcdaddm  16450  lcmdvds  16533  prmdvdsexp  16640  rpexp1i  16648  monpropd  17659  prfval  18120  xpcpropd  18129  curf2ndf  18168  eqglact  19106  ghmqusker  19214  mndodcongi  19470  oddvdsnn0  19471  efgi0  19647  efgi1  19648  efgsval2  19660  lss0cl  20896  mpofrlmd  21730  evls1fpws  22311  scmatscmid  22448  pmatcollpw3fi1lem1  22728  cnpval  23178  cnf2  23191  cnnei  23224  lfinun  23467  ptpjcn  23553  cnmptk2  23628  flfval  23932  cnmpt2plusg  24030  cnmpt2vsca  24137  ustincl  24150  xbln0  24356  blssec  24377  blpnfctr  24378  mopni2  24435  mopni3  24436  nmoval  24657  nmocl  24662  isnghm2  24666  isnmhm2  24694  cnmpt2ds  24786  metdseq0  24797  cnmpt2ip  25202  caucfil  25237  mbfimasn  25587  dvnf  25883  dvnbss  25884  coemul  26211  dvply1  26245  dvnply2  26249  pserdvlem2  26392  logeftb  26546  advlogexp  26618  cxpne0  26640  cxpp1  26643  elno2  27620  f1otrg  28892  ax5seglem9  28959  uhgrn0  29089  upgrn0  29111  upgrle  29112  uhgrwkspthlem2  29776  frgrhash2wsp  30356  sspval  30747  sspnval  30761  lnof  30779  nmooval  30787  nmooge0  30791  nmoub3i  30797  bloln  30808  nmblore  30810  hosval  31764  homval  31765  hodval  31766  hfsval  31767  hfmval  31768  homulass  31826  hoadddir  31828  nmopub2tALT  31933  nmfnleub2  31950  kbval  31978  lnopmul  31991  0lnfn  32009  lnopcoi  32027  nmcoplb  32054  nmcfnlb  32078  kbass2  32141  nmopleid  32163  hstoh  32256  mdi  32319  dmdi  32326  dmdi4  32331  tpssg  32561  fdifsuppconst  32717  supxrnemnf  32797  elrgspnlem2  33274  rloccring  33301  reofld  33373  nsgmgclem  33441  rhmimaidl  33462  dfufd2lem  33579  r1plmhm  33640  r1pquslmic  33641  lbsdiflsp0  33732  evls1fldgencl  33776  zarclsun  33976  zarclsint  33978  bnj605  35012  bnj607  35021  bnj1097  35086  fnrelpredd  35196  rankfilimb  35207  cusgredgex  35265  topdifinffinlem  37491  lindsdom  37754  lindsenlbs  37755  ftc1anclem2  37834  fzmul  37881  nninfnub  37891  exidreslem  38017  grposnOLD  38022  ghomf  38030  rngohomf  38106  rngohom1  38108  rngohomadd  38109  rngohommul  38110  rngoiso1o  38119  rngoisohom  38120  igenmin  38204  lkrcl  39291  lkrf0  39292  omlfh1N  39457  tendoex  41174  uzindd  42170  primrootsunit1  42290  sticksstones3  42341  sticksstones10  42348  sticksstones12a  42350  sticksstones12  42351  sticksstones17  42356  3anrabdioph  42966  3orrabdioph  42967  rencldnfilem  43004  dvdsabsmod0  43171  jm2.18  43172  jm2.25  43183  jm2.15nn0  43187  tfsconcatlem  43520  onsucunitp  43557  addrfv  44651  subrfv  44652  mulvfv  44653  bi3impa  44668  ssfiunibd  45499  supminfxr  45650  limsupgtlem  45963  xlimmnfv  46020  xlimpnfv  46024  dvnmul  46129  stoweidlem34  46220  stoweidlem48  46234  sge0cl  46567  sge0xp  46615  ovnsubaddlem1  46756  aovmpt4g  47389  gboge9  47952