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  3258  vtocl3gaf  3550  vtocl3ga  3552  rspc3v  3607  raltpg  4665  rextpg  4666  disjiun  5098  otthg  5448  3optocl  5738  fun2ssres  6564  funtpg  6574  funssfv  6882  f1elima  7241  ot1stg  7985  ot2ndg  7986  smogt  8339  omord2  8534  omword  8537  oeword  8557  omabslem  8617  ecovass  8800  fpmg  8844  findcard  9133  endjudisj  10129  cfsmolem  10230  ingru  10775  addasspi  10855  mulasspi  10857  ltapi  10863  ltmpi  10864  axpre-ltadd  11127  leltne  11270  dedekind  11344  recextlem2  11816  divdiv32  11897  divdiv1  11900  lble  12142  fnn0ind  12640  supminf  12901  xrleltne  13112  xrmaxeq  13146  xrmineq  13147  iccgelb  13370  elicc4  13381  iccsplit  13453  elfz  13481  modabs  13873  expgt0  14067  expge0  14070  expge1  14071  mulexpz  14074  expp1z  14083  expm1  14084  expmordi  14139  digit1  14209  faclbnd4  14269  faclbnd5  14270  ccatsymb  14554  s3eqs2s1eq  14911  abssubne0  15290  binom  15803  dvds0lem  16243  dvdsnegb  16250  muldvds1  16257  muldvds2  16258  dvdscmulr  16261  dvdsmulcr  16262  divalgmodcl  16384  gcd2n0cl  16486  gcdaddm  16502  lcmdvds  16585  prmdvdsexp  16692  rpexp1i  16700  monpropd  17706  prfval  18167  xpcpropd  18176  curf2ndf  18215  eqglact  19118  ghmqusker  19226  mndodcongi  19480  oddvdsnn0  19481  efgi0  19657  efgi1  19658  efgsval2  19670  lss0cl  20860  mpofrlmd  21693  evls1fpws  22263  scmatscmid  22400  pmatcollpw3fi1lem1  22680  cnpval  23130  cnf2  23143  cnnei  23176  lfinun  23419  ptpjcn  23505  cnmptk2  23580  flfval  23884  cnmpt2plusg  23982  cnmpt2vsca  24089  ustincl  24102  xbln0  24309  blssec  24330  blpnfctr  24331  mopni2  24388  mopni3  24389  nmoval  24610  nmocl  24615  isnghm2  24619  isnmhm2  24647  cnmpt2ds  24739  metdseq0  24750  cnmpt2ip  25155  caucfil  25190  mbfimasn  25540  dvnf  25836  dvnbss  25837  coemul  26164  dvply1  26198  dvnply2  26202  pserdvlem2  26345  logeftb  26499  advlogexp  26571  cxpne0  26593  cxpp1  26596  elno2  27573  f1otrg  28805  ax5seglem9  28871  uhgrn0  29001  upgrn0  29023  upgrle  29024  uhgrwkspthlem2  29691  frgrhash2wsp  30268  sspval  30659  sspnval  30673  lnof  30691  nmooval  30699  nmooge0  30703  nmoub3i  30709  bloln  30720  nmblore  30722  hosval  31676  homval  31677  hodval  31678  hfsval  31679  hfmval  31680  homulass  31738  hoadddir  31740  nmopub2tALT  31845  nmfnleub2  31862  kbval  31890  lnopmul  31903  0lnfn  31921  lnopcoi  31939  nmcoplb  31966  nmcfnlb  31990  kbass2  32053  nmopleid  32075  hstoh  32168  mdi  32231  dmdi  32238  dmdi4  32243  tpssg  32473  fdifsuppconst  32619  supxrnemnf  32698  elrgspnlem2  33201  rloccring  33228  reofld  33322  nsgmgclem  33389  rhmimaidl  33410  dfufd2lem  33527  r1plmhm  33582  r1pquslmic  33583  lbsdiflsp0  33629  evls1fldgencl  33672  zarclsun  33867  zarclsint  33869  bnj605  34904  bnj607  34913  bnj1097  34978  fnrelpredd  35086  cusgredgex  35116  topdifinffinlem  37342  lindsdom  37615  lindsenlbs  37616  ftc1anclem2  37695  fzmul  37742  nninfnub  37752  exidreslem  37878  grposnOLD  37883  ghomf  37891  rngohomf  37967  rngohom1  37969  rngohomadd  37970  rngohommul  37971  rngoiso1o  37980  rngoisohom  37981  igenmin  38065  lkrcl  39092  lkrf0  39093  omlfh1N  39258  tendoex  40976  uzindd  41972  primrootsunit1  42092  sticksstones3  42143  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  sticksstones17  42158  3anrabdioph  42777  3orrabdioph  42778  rencldnfilem  42815  dvdsabsmod0  42983  jm2.18  42984  jm2.25  42995  jm2.15nn0  42999  tfsconcatlem  43332  onsucunitp  43369  addrfv  44465  subrfv  44466  mulvfv  44467  bi3impa  44482  ssfiunibd  45314  supminfxr  45467  limsupgtlem  45782  xlimmnfv  45839  xlimpnfv  45843  dvnmul  45948  stoweidlem34  46039  stoweidlem48  46053  sge0cl  46386  sge0xp  46434  ovnsubaddlem1  46575  aovmpt4g  47206  gboge9  47769