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  1808  rspec3  3286  vtocl3gaf  3543  vtocl3ga  3544  rspc3v  3595  raltpg  4659  rextpg  4660  disjiun  5094  otthg  5458  3optocl  5753  fun2ssres  6594  funtpg  6606  funssfv  6917  f1elima  7277  mpt3fvot2d  7700  ot1stg  8025  ot2ndg  8026  smogt  8389  omord2  8589  omword  8592  oeword  8613  omabslem  8673  ecovass  8859  fpmg  8910  findcard  9193  endjudisj  10260  cfsmolem  10361  ingru  10913  addasspi  10993  mulasspi  10995  ltapi  11001  ltmpi  11002  axpre-ltadd  11265  leltne  11412  dedekind  11486  recextlem2  11960  divdiv32  12038  divdiv1  12041  lble  12282  fnn0ind  12811  supminf  13075  xrleltne  13287  xrmaxeq  13322  xrmineq  13323  iccgelb  13546  elicc4  13557  iccsplit  13629  elfz  13658  modabs  14057  expgt0  14251  expge0  14254  expge1  14255  mulexpz  14258  expp1z  14267  expm1  14268  expmordi  14323  digit1  14394  faclbnd4  14454  faclbnd5  14455  ccatsymb  14741  s3eqs2s1eq  15104  abssubne0  15499  binom  16014  dvds0lem  16451  dvdsnegb  16458  muldvds1  16465  muldvds2  16466  dvdscmulr  16469  dvdsmulcr  16470  divalgmodcl  16592  gcd2n0cl  16694  gcdaddm  16712  lcmdvds  16798  prmdvdsexp  16906  rpexp1i  16914  monpropd  17927  prfval  18388  xpcpropd  18397  curf2ndf  18436  eqglact  19406  ghmqusker  19516  mndodcongi  19772  oddvdsnn0  19773  efgi0  19949  efgi1  19950  efgsval2  19962  lss0cl  21237  mpofrlmd  22098  lindsdom  22171  lindsenlbs  22172  evls1fpws  22702  scmatscmid  22836  pmatcollpw3fi1lem1  23119  cnpval  23569  cnf2  23582  cnnei  23615  lfinun  23859  ptpjcn  23945  cnmptk2  24020  flfval  24324  cnmpt2plusg  24422  cnmpt2vsca  24529  ustincl  24542  xbln0  24748  blssec  24769  blpnfctr  24770  mopni2  24827  mopni3  24828  nmoval  25049  nmocl  25054  isnghm2  25058  isnmhm2  25086  cnmpt2ds  25178  metdseq0  25189  cnmpt2ip  25584  caucfil  25619  mbfimasn  25968  dvnf  26262  dvnbss  26263  coemul  26586  dvply1  26620  dvnply2  26623  pserdvlem2  26770  logeftb  26926  advlogexp  26998  cxpne0  27020  cxpp1  27023  elno2  28026  f1otrg  29463  ax5seglem9  29530  uhgrn0  29660  upgrn0  29682  upgrle  29683  uhgrwkspthlem2  30355  frgrhash2wsp  30948  sspval  31340  sspnval  31354  lnof  31372  nmooval  31380  nmooge0  31384  nmoub3i  31390  bloln  31401  nmblore  31403  hosval  32357  homval  32358  hodval  32359  hfsval  32360  hfmval  32361  homulass  32419  hoadddir  32421  nmopub2tALT  32526  nmfnleub2  32543  kbval  32571  lnopmul  32584  0lnfn  32602  lnopcoi  32620  nmcoplb  32647  nmcfnlb  32671  kbass2  32734  nmopleid  32756  hstoh  32849  mdi  32912  dmdi  32919  dmdi4  32924  tpssg  33190  fdifsuppconst  33339  supxrnemnf  33416  elrgspnlem2  33860  rloccring  33888  reofld  33960  nsgmgclem  34018  rhmimaidl  34038  dfufd2lem  34137  r1plmhm  34197  r1pquslmic  34198  lbsdiflsp0  34314  evls1fldgencl  34358  zarclsun  34558  zarclsint  34560  bnj605  35593  bnj607  35602  bnj1097  35667  soinfdom  35780  fnrelpredd  35784  rankfilimb  35792  cusgredgex  36020  topdifinffinlem  38416  ftc1anclem2  38758  fzmul  38821  nninfnub  38831  exidreslem  38957  grposnOLD  38962  ghomf  38970  rngohomf  39046  rngohom1  39048  rngohomadd  39049  rngohommul  39050  rngoiso1o  39059  rngoisohom  39060  igenmin  39144  lkrcl  40295  lkrf0  40296  omlfh1N  40461  tendoex  42178  uzindd  43174  primrootsunit1  43293  sticksstones3  43344  sticksstones10  43351  sticksstones12a  43353  sticksstones12  43354  sticksstones17  43359  3anrabdioph  43939  3orrabdioph  43940  rencldnfilem  43973  dvdsabsmod0  44140  jm2.18  44141  jm2.25  44152  jm2.15nn0  44156  tfsconcatlem  44484  onsucunitp  44521  addrfv  45596  subrfv  45597  mulvfv  45598  bi3impa  45613  ssfiunibd  46470  supminfxr  46619  limsupgtlem  46932  xlimmnfv  46989  xlimpnfv  46993  dvnmul  47098  stoweidlem34  47189  stoweidlem48  47203  sge0cl  47536  sge0xp  47584  ovnsubaddlem1  47725  aovmpt4g  48416  gboge9  49007