Theorem 19.20ii 971

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 968	. 2 |- (A.xph -> A.x(ps -> ch))
3		19.20 970	. 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 950

This theorem is referenced by:  19.20d 972  19.15 973  hbnt 978  19.22 1015  19.26 1043  dral1 1137  a4at 1141  cbv1 1145  sbied 1178  sbi1 1216  hbsb4 1232  sb9i 1247  sbal1 1328  immo 1394  2mo 1424  r19.20 1678  ralcom2 1752  sstr2 2042  difin0ss 2303  intss 2522

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-4 951  ax-5 952  ax-gen 955

Copyright terms: Public domain