Theorem 19.21ai 995

Description: Inference from Theorem 19.21 of [Margaris] p. 90.

Hypotheses

Ref	Expression
19.21ai.1	⊢ (φ → ∀xφ)
19.21ai.2	⊢ (φ → ψ)

Assertion

Ref	Expression
19.21ai	⊢ (φ → ∀xψ)

Proof of Theorem 19.21ai

Step	Hyp	Ref	Expression
1		19.21ai.1	. 2 ⊢ (φ → ∀xφ)
2		19.21ai.2	. . 3 ⊢ (φ → ψ)
3	2	19.20i 989	. 2 ⊢ (∀xφ → ∀xψ)
4	1, 3	syl 10	1 ⊢ (φ → ∀xψ)

Syntax hints:   → wi 3  ∀wal 951

This theorem is referenced by:  hbim 1004  19.12 1043  19.21 1052  19.21ad 1055  19.22d 1058  19.23 1059  19.23ad 1062  19.38 1077  nexd 1098  albid 1100  exbid 1101  hbnd 1105  ax11i 1134  sb6x 1184  equs5e 1194  aev 1204  sbbid 1241  dvelimdf 1246  sb6rf 1255  sb8 1256  a16g 1271  19.21aiv 1281  ax11f 1358  ax11indalem 1361  ax11inda2ALT 1362  a12lem1 1369  2moex 1433  2mo 1440  abbid 1568  r19.21ai 1704  ceqsalg 1816  ceqsex 1825  sbcbid 1966  csbeq2d 2008  hbcsb1g 2014  hbcsbg 2016  csbnestglem 2025  csbnest1g 2027  zfrepclf 2689  ssopab2 2811  dmcosseq 3349  imadif 3560  fnopabg 3601  hbfvd2 3716  axrepnd 4918  axunnd 4920  axpownd 4925  axregndlem1 4926  axacndlem1 4931  axacndlem2 4932  axacndlem3 4933  axacndlem4 4934  axacndlem5 4935  axacnd 4936  suppsr3 5196  chcmh 9034  homcard 10426  imonclem 10583  ismonc 10584

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

Copyright terms: Public domain