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

Theorem syl1111anc 838
 Description: Four-hypothesis elimination deduction for an assertion with a singleton virtual hypothesis collection. Similar to syl112anc 1372 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 515 . 2 (𝜑 → (𝜓𝜒))
4 syl1111anc.3 . 2 (𝜑𝜃)
5 syl1111anc.4 . 2 (𝜑𝜏)
6 syl1111anc.5 . 2 ((((𝜓𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜂)
73, 4, 5, 6syl21anc 836 1 (𝜑𝜂)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  mpsyl4anc  839  ucnima  22997  f1otrge  26780  swrdf1  30766  mgcf1o  30821  cycpmrn  30950  linds2eq  31110  rhmimaidl  31144  idlmulssprm  31152  isprmidlc  31158  prmidlc  31159  qsidomlem2  31164  lbsdiflsp0  31242  extdg1id  31273  3cubeslem1  40044  sineq0ALT  42062  cncfshift  42928  cncfperiod  42933
 Copyright terms: Public domain W3C validator