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  3606  reuss2  4285  reupick  4288  elinxp  5979  ordtr2  6365  suc11  6429  funimass4  6907  fliftfun  7269  omlimcl  8519  nneob  8597  rankwflemb  9722  cflm  10179  domtriomlem  10371  grothomex  10758  sup3  12116  caubnd  15301  fbflim2  23897  ellimc3  25813  usgruspgrb  29163  usgredgsscusgredg  29440  3cyclfrgrrn1  30264  dfon2lem6  35769  opnrebl2  36302  bj-nfimt  36619  axc11n11r  36664  bj-nnf-alrim  36736  stdpc5t  36808  wl-ax13lem1  37475  diaintclN  41045  dibintclN  41154  dihintcl  41331  sn-sup3d  42473  dflim5  43311  pm11.71  44379  axc11next  44388  rrx2plord2  48704