Theorem syl9 77

Description: A nested syllogism inference with different antecedents. (Contributed by NM, 13-May-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.)

Hypotheses

Ref	Expression
syl9.1	⊢ (𝜑 → (𝜓 → 𝜒))
syl9.2	⊢ (𝜃 → (𝜒 → 𝜏))

Assertion

Ref	Expression
syl9	⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))

Proof of Theorem syl9

Step	Hyp	Ref	Expression
1		syl9.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl9.2	. . 3 ⊢ (𝜃 → (𝜒 → 𝜏))
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜃 → (𝜒 → 𝜏)))
4	1, 3	syl5d 73	1 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl9r  78  com23  86  sylan9  503  19.38a  1938  ax13lem1  2391  ax13lem2  2393  axc11n  2447  sbequi  2506  reuss2  4136  reupick  4140  elinxp  5670  elresOLD  5672  ordtr2  6007  suc11  6066  funimass4  6494  fliftfun  6817  omlimcl  7925  nneob  7999  rankwflemb  8933  cflm  9387  domtriomlem  9579  grothomex  9966  sup3  11310  caubnd  14475  fbflim2  22151  ellimc3  24042  usgruspgrb  26480  usgredgsscusgredg  26757  3cyclfrgrrn1  27655  dfon2lem6  32220  opnrebl2  32843  bj-exlalrim  33122  bj-nfimt  33135  axc11n11r  33201  stdpc5t  33331  wl-ax13lem1  33827  diaintclN  37126  dibintclN  37235  dihintcl  37412  pm11.71  39430  axc11next  39439