Theorem 19.20ii 1036

Description: Inference quantifying antecedent, nested antecedent, and consequent.

Hypothesis

Ref	Expression
19.20ii.1	|- (ph -> (ps -> ch))

Assertion

Ref	Expression
19.20ii	|- (A.xph -> (A.xps -> A.xch))

Proof of Theorem 19.20ii

Step	Hyp	Ref	Expression
1		19.20ii.1	. . 3 |- (ph -> (ps -> ch))
2	1	19.20i 1033	. 2 |- (A.xph -> A.x(ps -> ch))
3		19.20 1035	. 2 |- (A.x(ps -> ch) -> (A.xps -> A.xch))
4	2, 3	syl 10	1 |- (A.xph -> (A.xps -> A.xch))

Syntax hints:   -> wi 3  A.wal 995

This theorem is referenced by:  19.20d 1037  19.15 1038  hbnt 1043  19.22 1080  19.26 1108  ax10o 1181  a4imt 1200  cbv1 1204  sbied 1237  sbi1 1274  hbsb4 1290  sb9i 1305  sbal1 1388  immo 1459  2mo 1490  r19.20 1749  ralcom2 1823  sstr2 2122  difin0ss 2384  intss 2608

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 1004  ax-4 1014  ax-5o 1016

Copyright terms: Public domain