Theorem syl9r 79

Description: A nested syllogism inference with different antecedents. (Contributed by NM, 14-May-1993.)

Hypotheses

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

Assertion

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

Proof of Theorem syl9r

Step	Hyp	Ref	Expression
1		syl9r.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl9r.2	. . 3 ⊢ (𝜃 → (𝜒 → 𝜏))
3	1, 2	syl9 78	. 2 ⊢ (𝜑 → (𝜃 → (𝜓 → 𝜏)))
4	3	com12 33	1 ⊢ (𝜃 → (𝜑 → (𝜓 → 𝜏)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  peirceroll  86  imim12  106  expt  178  sylan9r  518  19.38b  1874  ax12v2  2215  axprlem3  5390  fununi  6608  dfimafn  6940  funimass3  7046  isomin  7338  oneqmin  7799  tz7.48lem  8430  fisupg  9258  fiinfg  9471  trcl  9707  coflim  10263  coftr  10275  axdc3lem2  10453  konigthlem  10577  indpi  10916  nnsub  12304  2ndc1stc  23676  kgencn2  23783  tx1stc  23876  filuni  24111  fclscf  24251  alexsubALTlem2  24274  alexsubALTlem3  24275  alexsubALT  24277  nodenselem8  27927  n0subs  28628  lpni  30961  dfimafnf  33109  r1omhfb  35622  r1omhfbregs  35663  dfon2lem6  36365  bj-nnf-exlim  37493  finixpnum  38359  heiborlem4  38564  lncvrelatN  40654  imbi13  45343  relpmin  45775  dfaimafn  48053  sgoldbeven3prm  48699