Theorem bialdv 935

Description: Formula-building rule for universal quantifier (deduction rule).

Hypothesis

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

Assertion

Ref	Expression
bialdv	|- (ph -> (A.xps <-> A.xch))

Distinct variable group(s):   ph,x

Proof of Theorem bialdv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 |- (ph -> A.xph)
2		bialdv.1	. 2 |- (ph -> (ps <-> ch))
3	1, 2	biald 782	1 |- (ph -> (A.xps <-> A.xch))

Syntax hints:   -> wi 2   <-> wb 127  A.wal 672

This theorem is referenced by:  bi2aldv 937  sbcom2 992  euf 1011  mo 1020  axac 1085  zfext2 1087  bm1.1 1088  cleq1 1107  hblem 1170  biraldv2 1221  alexeq 1409  mo2icl 1434  sbc6g 1451  sbcal 1464  axrep 1473  axrep2 1474  zfrepclf 1477  bm1.3ii 1481  ssconb 1598  elint 1971  elinti 1974  freq1 2174  onminex 2275  dfom2 2374  elom 2375  elomg 2376  f1fv 2916  pssnn 3428  fiint 3445  inf0 3457  inf4 3473  tz9.1 3490  karden 3551  aceq0 3553  aceq5 3563  axpowndlem3 3745  zfcndrep 3760  zfcndac 3765  elnp 3886  prlem934 3933  suplem2pr 3956  suppr 3957  suppsr 4016  supsrlem6 4024  supre 4054  peano5nn 4424  nnwof 4609  chlim 5139

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org