Theorem 19.20ii 995

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 992	. 2 |- (A.xph -> A.x(ps -> ch))
3		19.20 994	. 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 954

This theorem is referenced by:  19.20d 996  19.15 997  hbnt 1002  19.22 1039  19.26 1067  ax10o 1139  a4imt 1158  cbv1 1162  sbied 1195  sbi1 1232  hbsb4 1248  sb9i 1263  sbal1 1346  immo 1417  2mo 1447  r19.20 1702  ralcom2 1776  sstr2 2071  difin0ss 2332  intss 2554

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975

Copyright terms: Public domain