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  507  19.38a  1840  ax13lem1  2372  ax13lem2  2374  axc11n  2424  rspc6v  3598  reuss2  4277  reupick  4280  elinxp  5970  ordtr2  6352  suc11  6416  funimass4  6887  fliftfun  7249  omlimcl  8496  nneob  8574  rankwflemb  9689  cflm  10144  domtriomlem  10336  grothomex  10723  sup3  12082  caubnd  15266  fbflim2  23862  ellimc3  25778  usgruspgrb  29132  usgredgsscusgredg  29409  3cyclfrgrrn1  30233  dfon2lem6  35782  opnrebl2  36315  bj-nfimt  36632  axc11n11r  36677  bj-nnf-alrim  36749  stdpc5t  36821  wl-ax13lem1  37488  diaintclN  41057  dibintclN  41166  dihintcl  41343  sn-sup3d  42485  dflim5  43322  pm11.71  44390  axc11next  44399  rrx2plord2  48727