Theorem 3impa 1127

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-3an 1105

This theorem is used by:  3imp  1128  3adant1  1148  3adant2  1149  ex3  1365  3impdir  1370  syl3an9b  1462  biimp3a  1498  stoic3  1809  rspec3  3283  vtocl3gaf  3540  vtocl3ga  3541  rspc3v  3592  raltpg  4659  rextpg  4660  disjiun  5091  otthg  5454  3optocl  5748  fun2ssres  6585  funtpg  6595  funssfv  6906  f1elima  7267  mpt3fvot2d  7690  ot1stg  8015  ot2ndg  8016  smogt  8375  omord2  8575  omword  8578  oeword  8599  omabslem  8659  ecovass  8845  fpmg  8896  findcard  9179  endjudisj  10247  cfsmolem  10348  ingru  10900  addasspi  10980  mulasspi  10982  ltapi  10988  ltmpi  10989  axpre-ltadd  11252  leltne  11399  dedekind  11473  recextlem2  11947  divdiv32  12025  divdiv1  12028  lble  12269  fnn0ind  12798  supminf  13062  xrleltne  13274  xrmaxeq  13309  xrmineq  13310  iccgelb  13533  elicc4  13544  iccsplit  13616  elfz  13645  modabs  14044  expgt0  14238  expge0  14241  expge1  14242  mulexpz  14245  expp1z  14254  expm1  14255  expmordi  14310  digit1  14381  faclbnd4  14441  faclbnd5  14442  ccatsymb  14728  s3eqs2s1eq  15089  abssubne0  15484  binom  15999  dvds0lem  16436  dvdsnegb  16443  muldvds1  16450  muldvds2  16451  dvdscmulr  16454  dvdsmulcr  16455  divalgmodcl  16577  gcd2n0cl  16679  gcdaddm  16697  lcmdvds  16783  prmdvdsexp  16891  rpexp1i  16899  monpropd  17912  prfval  18373  xpcpropd  18382  curf2ndf  18421  eqglact  19391  ghmqusker  19501  mndodcongi  19757  oddvdsnn0  19758  efgi0  19934  efgi1  19935  efgsval2  19947  lss0cl  21222  mpofrlmd  22083  lindsdom  22156  lindsenlbs  22157  evls1fpws  22687  scmatscmid  22821  pmatcollpw3fi1lem1  23104  cnpval  23554  cnf2  23567  cnnei  23600  lfinun  23844  ptpjcn  23930  cnmptk2  24005  flfval  24309  cnmpt2plusg  24407  cnmpt2vsca  24514  ustincl  24527  xbln0  24733  blssec  24754  blpnfctr  24755  mopni2  24812  mopni3  24813  nmoval  25034  nmocl  25039  isnghm2  25043  isnmhm2  25071  cnmpt2ds  25163  metdseq0  25174  cnmpt2ip  25569  caucfil  25604  mbfimasn  25953  dvnf  26247  dvnbss  26248  coemul  26571  dvply1  26605  dvnply2  26608  pserdvlem2  26755  logeftb  26911  advlogexp  26983  cxpne0  27005  cxpp1  27008  elno2  28011  f1otrg  29448  ax5seglem9  29515  uhgrn0  29645  upgrn0  29667  upgrle  29668  uhgrwkspthlem2  30340  frgrhash2wsp  30933  sspval  31325  sspnval  31339  lnof  31357  nmooval  31365  nmooge0  31369  nmoub3i  31375  bloln  31386  nmblore  31388  hosval  32342  homval  32343  hodval  32344  hfsval  32345  hfmval  32346  homulass  32404  hoadddir  32406  nmopub2tALT  32511  nmfnleub2  32528  kbval  32556  lnopmul  32569  0lnfn  32587  lnopcoi  32605  nmcoplb  32632  nmcfnlb  32656  kbass2  32719  nmopleid  32741  hstoh  32834  mdi  32897  dmdi  32904  dmdi4  32909  tpssg  33133  fdifsuppconst  33282  supxrnemnf  33360  elrgspnlem2  33804  rloccring  33832  reofld  33904  nsgmgclem  33962  rhmimaidl  33982  dfufd2lem  34081  r1plmhm  34141  r1pquslmic  34142  lbsdiflsp0  34258  evls1fldgencl  34302  zarclsun  34502  zarclsint  34504  bnj605  35537  bnj607  35546  bnj1097  35611  soinfdom  35717  fnrelpredd  35720  rankfilimb  35728  cusgredgex  35906  topdifinffinlem  38270  ftc1anclem2  38612  fzmul  38675  nninfnub  38685  exidreslem  38811  grposnOLD  38816  ghomf  38824  rngohomf  38900  rngohom1  38902  rngohomadd  38903  rngohommul  38904  rngoiso1o  38913  rngoisohom  38914  igenmin  38998  lkrcl  40149  lkrf0  40150  omlfh1N  40315  tendoex  42032  uzindd  43028  primrootsunit1  43147  sticksstones3  43198  sticksstones10  43205  sticksstones12a  43207  sticksstones12  43208  sticksstones17  43213  3anrabdioph  43792  3orrabdioph  43793  rencldnfilem  43826  dvdsabsmod0  43993  jm2.18  43994  jm2.25  44005  jm2.15nn0  44009  tfsconcatlem  44337  onsucunitp  44374  addrfv  45450  subrfv  45451  mulvfv  45452  bi3impa  45467  ssfiunibd  46324  supminfxr  46473  limsupgtlem  46786  xlimmnfv  46843  xlimpnfv  46847  dvnmul  46952  stoweidlem34  47043  stoweidlem48  47057  sge0cl  47390  sge0xp  47438  ovnsubaddlem1  47579  aovmpt4g  48270  gboge9  48861