Theorem syl9 75

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 71	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  76  com23  84  sylan9  687  19.21t  2061  19.21t-1OLD  2200  ax13lem1  2236  ax13lem2  2284  axc11n  2295  axc11nOLD  2296  axc11nOLDOLD  2297  axc11nALT  2298  sbequi  2363  reuss2  3866  reupick  3870  elres  5355  ordtr2  5685  suc11  5748  funimass4  6157  fliftfun  6462  omlimcl  7545  nneob  7619  rankwflemb  8539  cflm  8955  domtriomlem  9147  grothomex  9530  sup3  10859  caubnd  13946  fbflim2  21591  ellimc3  23449  3cyclfrgrarn1  26539  dfon2lem6  30937  opnrebl2  31486  axc11n11r  31860  stdpc5t  32002  bj-nfimt  32025  wl-ax13lem1  32466  diaintclN  35365  dibintclN  35474  dihintcl  35651  pm11.71  37619  axc11next  37629  usgruspgrb  40411  usgredgsscusgredg  40675  3cyclfrgrrn1  41455