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 216	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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-3an 1088

This theorem is referenced by:  3imp  1110  3adant1  1129  3adant2  1130  ex3  1345  3impdir  1350  syl3an9b  1433  biimp3a  1468  stoic3  1779  rspec3  3138  rspc3v  3574  raltpg  4635  rextpg  4636  disjiun  5062  otthg  5401  3optocl  5684  fun2ssres  6486  funtpg  6496  funssfv  6804  f1elima  7145  ot1stg  7854  ot2ndg  7855  smogt  8207  omord2  8407  omword  8410  oeword  8430  omabslem  8489  ecovass  8622  fpmg  8665  findcard  8955  endjudisj  9933  cfsmolem  10035  ingru  10580  addasspi  10660  mulasspi  10662  ltapi  10668  ltmpi  10669  axpre-ltadd  10932  leltne  11073  dedekind  11147  recextlem2  11615  divdiv32  11692  divdiv1  11695  lble  11936  fnn0ind  12428  supminf  12684  xrleltne  12888  xrmaxeq  12922  xrmineq  12923  iccgelb  13144  elicc4  13155  iccsplit  13226  elfz  13254  modabs  13633  expgt0  13825  expge0  13828  expge1  13829  mulexpz  13832  expp1z  13841  expm1  13842  expmordi  13894  digit1  13961  faclbnd4  14020  faclbnd5  14021  ccatsymb  14296  s3eqs2s1eq  14660  abssubne0  15037  binom  15551  dvds0lem  15985  dvdsnegb  15992  muldvds1  15999  muldvds2  16000  dvdscmulr  16003  dvdsmulcr  16004  divalgmodcl  16125  gcd2n0cl  16225  gcdaddm  16241  lcmdvds  16322  prmdvdsexp  16429  rpexp1i  16437  monpropd  17458  prfval  17925  xpcpropd  17935  curf2ndf  17974  eqglact  18816  mndodcongi  19160  oddvdsnn0  19161  efgi0  19335  efgi1  19336  efgsval2  19348  lss0cl  20217  mpofrlmd  20993  scmatscmid  21664  pmatcollpw3fi1lem1  21944  cnpval  22396  cnf2  22409  cnnei  22442  lfinun  22685  ptpjcn  22771  cnmptk2  22846  flfval  23150  cnmpt2plusg  23248  cnmpt2vsca  23355  ustincl  23368  xbln0  23576  blssec  23597  blpnfctr  23598  mopni2  23658  mopni3  23659  nmoval  23888  nmocl  23893  isnghm2  23897  isnmhm2  23925  cnmpt2ds  24015  metdseq0  24026  cnmpt2ip  24421  caucfil  24456  mbfimasn  24805  dvnf  25100  dvnbss  25101  coemul  25422  dvply1  25453  dvnply2  25456  pserdvlem2  25596  logeftb  25748  advlogexp  25819  cxpne0  25841  cxpp1  25844  f1otrg  27241  ax5seglem9  27314  uhgrn0  27446  upgrn0  27468  upgrle  27469  uhgrwkspthlem2  28131  frgrhash2wsp  28705  sspval  29094  sspnval  29108  lnof  29126  nmooval  29134  nmooge0  29138  nmoub3i  29144  bloln  29155  nmblore  29157  hosval  30111  homval  30112  hodval  30113  hfsval  30114  hfmval  30115  homulass  30173  hoadddir  30175  nmopub2tALT  30280  nmfnleub2  30297  kbval  30325  lnopmul  30338  0lnfn  30356  lnopcoi  30374  nmcoplb  30401  nmcfnlb  30425  kbass2  30488  nmopleid  30510  hstoh  30603  mdi  30666  dmdi  30673  dmdi4  30678  fdifsuppconst  31032  supxrnemnf  31100  reofld  31553  nsgmgclem  31605  rhmimaidl  31618  lbsdiflsp0  31716  zarclsun  31829  zarclsint  31831  bnj605  32896  bnj607  32905  bnj1097  32970  fnrelpredd  33070  cusgredgex  33092  elno2  33866  topdifinffinlem  35527  lindsdom  35780  lindsenlbs  35781  ftc1anclem2  35860  fzmul  35908  nninfnub  35918  exidreslem  36044  grposnOLD  36049  ghomf  36057  rngohomf  36133  rngohom1  36135  rngohomadd  36136  rngohommul  36137  rngoiso1o  36146  rngoisohom  36147  igenmin  36231  lkrcl  37113  lkrf0  37114  omlfh1N  37279  tendoex  38996  uzindd  39992  sticksstones3  40111  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  sticksstones17  40126  3anrabdioph  40611  3orrabdioph  40612  rencldnfilem  40649  dvdsabsmod0  40816  jm2.18  40817  jm2.25  40828  jm2.15nn0  40832  addrfv  42094  subrfv  42095  mulvfv  42096  bi3impa  42111  ssfiunibd  42855  supminfxr  43011  limsupgtlem  43325  xlimmnfv  43382  xlimpnfv  43386  dvnmul  43491  stoweidlem34  43582  stoweidlem48  43596  sge0cl  43926  sge0xp  43974  ovnsubaddlem1  44115  aovmpt4g  44704  gboge9  45227