MPE Home 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 1374 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 512 . 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 396
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 206  df-an 397
This theorem is referenced by:  mpsyl4anc  840  ucnima  23793  f1otrge  28161  swrdf1  32158  mgcf1o  32211  cycpmrn  32343  linds2eq  32542  rhmimaidl  32595  idlmulssprm  32605  isprmidlc  32611  prmidlc  32612  qsidomlem2  32617  lbsdiflsp0  32770  extdg1id  32801  3cubeslem1  41504  cantnftermord  42152  sineq0ALT  43780  cncfshift  44669  cncfperiod  44674
  Copyright terms: Public domain W3C validator