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  1842  ax13lem1  2379  ax13lem2  2381  axc11n  2431  rspc6v  3586  reuss2  4267  reupick  4270  axprglem  5374  elinxp  5979  ordtr2  6363  suc11  6427  funimass4  6899  fliftfun  7261  omlimcl  8507  nneob  8586  rankwflemb  9711  cflm  10166  domtriomlem  10358  grothomex  10746  sup3  12107  caubnd  15315  fbflim2  23955  ellimc3  25859  usgruspgrb  29269  usgredgsscusgredg  29546  3cyclfrgrrn1  30373  dfon2lem6  35987  opnrebl2  36522  axtco1from2  36676  bj-nfimt  36936  axc11n11r  36999  bj-nnf-alrim  37061  stdpc5t  37153  wl-ax13lem1  37827  diaintclN  41521  dibintclN  41630  dihintcl  41807  sn-sup3d  42954  dflim5  43778  pm11.71  44845  axc11next  44854  rrx2plord2  49213