Theorem 3impa 1123

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099

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 209  df-3an 1101

This theorem is referenced by:  3imp  1124  3adant1  1144  3adant2  1145  ex3  1361  3impdir  1366  syl3an9b  1457  biimp3a  1492  stoic3  1798  rspec3  3284  vtocl3gaf  3546  vtocl3ga  3547  rspc3v  3599  raltpg  4659  rextpg  4660  disjiun  5090  otthg  5455  3optocl  5746  fun2ssres  6568  funtpg  6578  funssfv  6890  f1elima  7249  ot1stg  7986  ot2ndg  7987  smogt  8340  omord2  8538  omword  8541  oeword  8562  omabslem  8622  ecovass  8808  fpmg  8852  findcard  9134  endjudisj  10127  cfsmolem  10229  ingru  10775  addasspi  10855  mulasspi  10857  ltapi  10863  ltmpi  10864  axpre-ltadd  11127  leltne  11274  dedekind  11348  recextlem2  11820  divdiv32  11901  divdiv1  11904  lble  12146  fnn0ind  12674  supminf  12938  xrleltne  13149  xrmaxeq  13184  xrmineq  13185  iccgelb  13408  elicc4  13419  iccsplit  13491  elfz  13520  modabs  13916  expgt0  14110  expge0  14113  expge1  14114  mulexpz  14117  expp1z  14126  expm1  14127  expmordi  14182  digit1  14252  faclbnd4  14312  faclbnd5  14313  ccatsymb  14598  s3eqs2s1eq  14953  abssubne0  15346  binom  15862  dvds0lem  16302  dvdsnegb  16309  muldvds1  16316  muldvds2  16317  dvdscmulr  16320  dvdsmulcr  16321  divalgmodcl  16443  gcd2n0cl  16545  gcdaddm  16561  lcmdvds  16644  prmdvdsexp  16752  rpexp1i  16760  monpropd  17772  prfval  18233  xpcpropd  18242  curf2ndf  18281  eqglact  19222  ghmqusker  19329  mndodcongi  19585  oddvdsnn0  19586  efgi0  19762  efgi1  19763  efgsval2  19775  lss0cl  21016  mpofrlmd  21831  evls1fpws  22434  scmatscmid  22568  pmatcollpw3fi1lem1  22848  cnpval  23298  cnf2  23311  cnnei  23344  lfinun  23587  ptpjcn  23673  cnmptk2  23748  flfval  24052  cnmpt2plusg  24150  cnmpt2vsca  24257  ustincl  24270  xbln0  24476  blssec  24497  blpnfctr  24498  mopni2  24555  mopni3  24556  nmoval  24777  nmocl  24782  isnghm2  24786  isnmhm2  24814  cnmpt2ds  24906  metdseq0  24917  cnmpt2ip  25312  caucfil  25347  mbfimasn  25696  dvnf  25991  dvnbss  25992  coemul  26314  dvply1  26350  dvnply2  26353  pserdvlem2  26493  logeftb  26650  advlogexp  26722  cxpne0  26744  cxpp1  26747  elno2  27720  f1otrg  29073  ax5seglem9  29140  uhgrn0  29270  upgrn0  29292  upgrle  29293  uhgrwkspthlem2  29956  frgrhash2wsp  30536  sspval  30928  sspnval  30942  lnof  30960  nmooval  30968  nmooge0  30972  nmoub3i  30978  bloln  30989  nmblore  30991  hosval  31945  homval  31946  hodval  31947  hfsval  31948  hfmval  31949  homulass  32007  hoadddir  32009  nmopub2tALT  32114  nmfnleub2  32131  kbval  32159  lnopmul  32172  0lnfn  32190  lnopcoi  32208  nmcoplb  32235  nmcfnlb  32259  kbass2  32322  nmopleid  32344  hstoh  32437  mdi  32500  dmdi  32507  dmdi4  32512  tpssg  32738  fdifsuppconst  32893  supxrnemnf  32972  elrgspnlem2  33426  rloccring  33454  reofld  33531  nsgmgclem  33599  rhmimaidl  33620  dfufd2lem  33747  r1plmhm  33808  r1pquslmic  33809  lbsdiflsp0  33925  evls1fldgencl  33969  zarclsun  34169  zarclsint  34171  bnj605  35204  bnj607  35213  bnj1097  35278  fnrelpredd  35389  rankfilimb  35402  cusgredgex  35477  topdifinffinlem  37846  lindsdom  38118  lindsenlbs  38119  ftc1anclem2  38198  fzmul  38245  nninfnub  38255  exidreslem  38381  grposnOLD  38386  ghomf  38394  rngohomf  38470  rngohom1  38472  rngohomadd  38473  rngohommul  38474  rngoiso1o  38483  rngoisohom  38484  igenmin  38568  lkrcl  39721  lkrf0  39722  omlfh1N  39887  tendoex  41604  uzindd  42600  primrootsunit1  42719  sticksstones3  42770  sticksstones10  42777  sticksstones12a  42779  sticksstones12  42780  sticksstones17  42785  3anrabdioph  43368  3orrabdioph  43369  rencldnfilem  43402  dvdsabsmod0  43569  jm2.18  43570  jm2.25  43581  jm2.15nn0  43585  tfsconcatlem  43918  onsucunitp  43955  addrfv  45049  subrfv  45050  mulvfv  45051  bi3impa  45066  ssfiunibd  45893  supminfxr  46043  limsupgtlem  46356  xlimmnfv  46413  xlimpnfv  46417  dvnmul  46522  stoweidlem34  46613  stoweidlem48  46627  sge0cl  46960  sge0xp  47008  ovnsubaddlem1  47149  aovmpt4g  47800  gboge9  48391