MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl1111anc Structured version   Visualization version   GIF version

Theorem syl1111anc 840
Description: Four-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc 1373 except the unification theorem uses left-nested conjunction. (Contributed by Alan Sare, 17-Oct-2017.)
Hypotheses
Ref Expression
syl1111anc.1 (𝜑𝜓)
syl1111anc.2 (𝜑𝜒)
syl1111anc.3 (𝜑𝜃)
syl1111anc.4 (𝜑𝜏)
syl1111anc.5 ((((𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)
Assertion
Ref Expression
syl1111anc (𝜑𝜂)

Proof of Theorem syl1111anc
StepHypRef Expression
1 syl1111anc.1 . . 3 (𝜑𝜓)
2 syl1111anc.2 . . 3 (𝜑𝜒)
31, 2jca 511 . 2 (𝜑 → (𝜓𝜒))
4 syl1111anc.3 . 2 (𝜑𝜃)
5 syl1111anc.4 . 2 (𝜑𝜏)
6 syl1111anc.5 . 2 ((((𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)
73, 4, 5, 6syl21anc 838 1 (𝜑𝜂)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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-an 396
This theorem is referenced by:  mpsyl4anc  842  ucnima  24306  f1otrge  28895  swrdf1  32926  mgcf1o  32978  chnind  32985  gsumfs2d  33041  cycpmrn  33146  linds2eq  33389  rhmimaidl  33440  idlmulssprm  33450  isprmidlc  33455  prmidlc  33456  qsidomlem2  33461  ply1unit  33580  lbsdiflsp0  33654  extdg1id  33691  3cubeslem1  42672  cantnftermord  43310  sineq0ALT  44935  cncfshift  45830  cncfperiod  45835
  Copyright terms: Public domain W3C validator