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  3287  vtocl3gaf  3546  vtocl3ga  3547  rspc3v  3599  raltpg  4666  rextpg  4667  disjiun  5099  otthg  5469  3optocl  5760  fun2ssres  6585  funtpg  6595  funssfv  6906  f1elima  7266  ot1stg  8006  ot2ndg  8007  smogt  8360  omord2  8558  omword  8561  oeword  8582  omabslem  8642  ecovass  8828  fpmg  8872  findcard  9155  endjudisj  10168  cfsmolem  10269  ingru  10819  addasspi  10899  mulasspi  10901  ltapi  10907  ltmpi  10908  axpre-ltadd  11171  leltne  11318  dedekind  11392  recextlem2  11864  divdiv32  11942  divdiv1  11945  lble  12186  fnn0ind  12715  supminf  12979  xrleltne  13190  xrmaxeq  13225  xrmineq  13226  iccgelb  13449  elicc4  13460  iccsplit  13532  elfz  13561  modabs  13959  expgt0  14153  expge0  14156  expge1  14157  mulexpz  14160  expp1z  14169  expm1  14170  expmordi  14225  digit1  14295  faclbnd4  14355  faclbnd5  14356  ccatsymb  14642  s3eqs2s1eq  15003  abssubne0  15396  binom  15911  dvds0lem  16350  dvdsnegb  16357  muldvds1  16364  muldvds2  16365  dvdscmulr  16368  dvdsmulcr  16369  divalgmodcl  16491  gcd2n0cl  16593  gcdaddm  16609  lcmdvds  16692  prmdvdsexp  16800  rpexp1i  16808  monpropd  17820  prfval  18281  xpcpropd  18290  curf2ndf  18329  eqglact  19295  ghmqusker  19405  mndodcongi  19661  oddvdsnn0  19662  efgi0  19838  efgi1  19839  efgsval2  19851  lss0cl  21122  mpofrlmd  21981  evls1fpws  22583  scmatscmid  22717  pmatcollpw3fi1lem1  22997  cnpval  23447  cnf2  23460  cnnei  23493  lfinun  23737  ptpjcn  23823  cnmptk2  23898  flfval  24202  cnmpt2plusg  24300  cnmpt2vsca  24407  ustincl  24420  xbln0  24626  blssec  24647  blpnfctr  24648  mopni2  24705  mopni3  24706  nmoval  24927  nmocl  24932  isnghm2  24936  isnmhm2  24964  cnmpt2ds  25056  metdseq0  25067  cnmpt2ip  25462  caucfil  25497  mbfimasn  25846  dvnf  26141  dvnbss  26142  coemul  26464  dvply1  26500  dvnply2  26503  pserdvlem2  26646  logeftb  26803  advlogexp  26875  cxpne0  26897  cxpp1  26900  elno2  27873  f1otrg  29279  ax5seglem9  29346  uhgrn0  29476  upgrn0  29498  upgrle  29499  uhgrwkspthlem2  30171  frgrhash2wsp  30758  sspval  31150  sspnval  31164  lnof  31182  nmooval  31190  nmooge0  31194  nmoub3i  31200  bloln  31211  nmblore  31213  hosval  32167  homval  32168  hodval  32169  hfsval  32170  hfmval  32171  homulass  32229  hoadddir  32231  nmopub2tALT  32336  nmfnleub2  32353  kbval  32381  lnopmul  32394  0lnfn  32412  lnopcoi  32430  nmcoplb  32457  nmcfnlb  32481  kbass2  32544  nmopleid  32566  hstoh  32659  mdi  32722  dmdi  32729  dmdi4  32734  tpssg  32958  fdifsuppconst  33109  supxrnemnf  33187  elrgspnlem2  33631  rloccring  33659  reofld  33731  nsgmgclem  33788  rhmimaidl  33808  dfufd2lem  33907  r1plmhm  33967  r1pquslmic  33968  lbsdiflsp0  34084  evls1fldgencl  34128  zarclsun  34328  zarclsint  34330  bnj605  35364  bnj607  35373  bnj1097  35438  fnrelpredd  35544  rankfilimb  35558  cusgredgex  35668  topdifinffinlem  38054  lindsdom  38326  lindsenlbs  38327  ftc1anclem2  38406  fzmul  38454  nninfnub  38464  exidreslem  38590  grposnOLD  38595  ghomf  38603  rngohomf  38679  rngohom1  38681  rngohomadd  38682  rngohommul  38683  rngoiso1o  38692  rngoisohom  38693  igenmin  38777  lkrcl  39928  lkrf0  39929  omlfh1N  40094  tendoex  41811  uzindd  42807  primrootsunit1  42926  sticksstones3  42977  sticksstones10  42984  sticksstones12a  42986  sticksstones12  42987  sticksstones17  42992  3anrabdioph  43590  3orrabdioph  43591  rencldnfilem  43624  dvdsabsmod0  43791  jm2.18  43792  jm2.25  43803  jm2.15nn0  43807  tfsconcatlem  44140  onsucunitp  44177  addrfv  45254  subrfv  45255  mulvfv  45256  bi3impa  45271  ssfiunibd  46105  supminfxr  46255  limsupgtlem  46568  xlimmnfv  46625  xlimpnfv  46629  dvnmul  46734  stoweidlem34  46825  stoweidlem48  46839  sge0cl  47172  sge0xp  47220  ovnsubaddlem1  47361  aovmpt4g  48015  gboge9  48606