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  1776  rspec3  3262  vtocl3gaf  3560  vtocl3ga  3562  rspc3v  3617  raltpg  4674  rextpg  4675  disjiun  5107  otthg  5460  3optocl  5751  fun2ssres  6580  funtpg  6590  funssfv  6896  f1elima  7255  ot1stg  8000  ot2ndg  8001  smogt  8379  omord2  8577  omword  8580  oeword  8600  omabslem  8660  ecovass  8836  fpmg  8880  findcard  9175  endjudisj  10181  cfsmolem  10282  ingru  10827  addasspi  10907  mulasspi  10909  ltapi  10915  ltmpi  10916  axpre-ltadd  11179  leltne  11322  dedekind  11396  recextlem2  11866  divdiv32  11947  divdiv1  11950  lble  12192  fnn0ind  12690  supminf  12949  xrleltne  13159  xrmaxeq  13193  xrmineq  13194  iccgelb  13417  elicc4  13428  iccsplit  13500  elfz  13528  modabs  13919  expgt0  14111  expge0  14114  expge1  14115  mulexpz  14118  expp1z  14127  expm1  14128  expmordi  14183  digit1  14253  faclbnd4  14313  faclbnd5  14314  ccatsymb  14598  s3eqs2s1eq  14955  abssubne0  15333  binom  15844  dvds0lem  16284  dvdsnegb  16291  muldvds1  16298  muldvds2  16299  dvdscmulr  16302  dvdsmulcr  16303  divalgmodcl  16424  gcd2n0cl  16526  gcdaddm  16542  lcmdvds  16625  prmdvdsexp  16732  rpexp1i  16740  monpropd  17748  prfval  18209  xpcpropd  18218  curf2ndf  18257  eqglact  19160  ghmqusker  19268  mndodcongi  19522  oddvdsnn0  19523  efgi0  19699  efgi1  19700  efgsval2  19712  lss0cl  20902  mpofrlmd  21735  evls1fpws  22305  scmatscmid  22442  pmatcollpw3fi1lem1  22722  cnpval  23172  cnf2  23185  cnnei  23218  lfinun  23461  ptpjcn  23547  cnmptk2  23622  flfval  23926  cnmpt2plusg  24024  cnmpt2vsca  24131  ustincl  24144  xbln0  24351  blssec  24372  blpnfctr  24373  mopni2  24430  mopni3  24431  nmoval  24652  nmocl  24657  isnghm2  24661  isnmhm2  24689  cnmpt2ds  24781  metdseq0  24792  cnmpt2ip  25198  caucfil  25233  mbfimasn  25583  dvnf  25879  dvnbss  25880  coemul  26207  dvply1  26241  dvnply2  26245  pserdvlem2  26388  logeftb  26542  advlogexp  26614  cxpne0  26636  cxpp1  26639  elno2  27616  f1otrg  28796  ax5seglem9  28862  uhgrn0  28992  upgrn0  29014  upgrle  29015  uhgrwkspthlem2  29682  frgrhash2wsp  30259  sspval  30650  sspnval  30664  lnof  30682  nmooval  30690  nmooge0  30694  nmoub3i  30700  bloln  30711  nmblore  30713  hosval  31667  homval  31668  hodval  31669  hfsval  31670  hfmval  31671  homulass  31729  hoadddir  31731  nmopub2tALT  31836  nmfnleub2  31853  kbval  31881  lnopmul  31894  0lnfn  31912  lnopcoi  31930  nmcoplb  31957  nmcfnlb  31981  kbass2  32044  nmopleid  32066  hstoh  32159  mdi  32222  dmdi  32229  dmdi4  32234  tpssg  32464  fdifsuppconst  32612  supxrnemnf  32691  elrgspnlem2  33184  rloccring  33211  reofld  33305  nsgmgclem  33372  rhmimaidl  33393  dfufd2lem  33510  r1plmhm  33565  r1pquslmic  33566  lbsdiflsp0  33612  evls1fldgencl  33657  zarclsun  33847  zarclsint  33849  bnj605  34884  bnj607  34893  bnj1097  34958  fnrelpredd  35066  cusgredgex  35090  topdifinffinlem  37311  lindsdom  37584  lindsenlbs  37585  ftc1anclem2  37664  fzmul  37711  nninfnub  37721  exidreslem  37847  grposnOLD  37852  ghomf  37860  rngohomf  37936  rngohom1  37938  rngohomadd  37939  rngohommul  37940  rngoiso1o  37949  rngoisohom  37950  igenmin  38034  lkrcl  39056  lkrf0  39057  omlfh1N  39222  tendoex  40940  uzindd  41936  primrootsunit1  42056  sticksstones3  42107  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  sticksstones17  42122  3anrabdioph  42752  3orrabdioph  42753  rencldnfilem  42790  dvdsabsmod0  42958  jm2.18  42959  jm2.25  42970  jm2.15nn0  42974  tfsconcatlem  43307  onsucunitp  43344  addrfv  44441  subrfv  44442  mulvfv  44443  bi3impa  44458  ssfiunibd  45286  supminfxr  45439  limsupgtlem  45754  xlimmnfv  45811  xlimpnfv  45815  dvnmul  45920  stoweidlem34  46011  stoweidlem48  46025  sge0cl  46358  sge0xp  46406  ovnsubaddlem1  46547  aovmpt4g  47178  gboge9  47726