Theorem al2imi 1341

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

Hypothesis

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

Assertion

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

Proof of Theorem al2imi

Step	Hyp	Ref	Expression
1		al2imi.1	. . 3 |- (ph -> (ps -> ch))
2	1	alimi 1338	. 2 |- (A.xph -> A.x(ps -> ch))
3		alim 1340	. 2 |- (A.x(ps -> ch) -> (A.xps -> A.xch))
4	2, 3	syl 12	1 |- (A.xph -> (A.xps -> A.xch))

Syntax hints:   -> wi 3  A.wal 1296

This theorem is referenced by:  alanimi 1342  alimd 1343  albi 1344  hbnt 1349  exim 1386  19.26 1416  ax10o 1499  a4imt 1519  cbv1 1523  sbiedOLD 1564  sbi1 1602  hbsb4 1620  sb9i 1640  sbal1 1737  immo 1813  2mo 1851  ralim 2164  ralcom2 2244  ralcom2OLD 2245  sstr2OLD 2624  difin0ss 2939  intss 3239  hbntg 13872  pm10.56 16317  pm10.57 16318  2al2imi 16320

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

Copyright terms: Public domain