Theorem albidv 1745

Description: Formula-building rule for universal quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
albidv.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
albidv	⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem albidv

Step	Hyp	Ref	Expression
1		ax-17 1459	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		albidv.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	albidh 1409	1 ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 103  ∀wal 1282

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-17 1459

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ax11v  1748  2albidv  1788  sbal1yz  1918  eujust  1943  euf  1946  mo23  1982  axext3  2064  bm1.1  2066  eqeq1  2087  nfceqdf  2218  ralbidv2  2370  alexeq  2721  pm13.183  2732  eqeu  2762  mo2icl  2771  euind  2779  reuind  2795  cdeqal  2804  sbcal  2865  sbcalg  2866  sbcabel  2895  csbiebg  2945  ssconb  3105  reldisj  3295  sbcssg  3350  elint  3642  axsep2  3897  zfauscl  3898  bm1.3ii  3899  euotd  4009  freq1  4099  freq2  4101  eusv1  4202  ontr2exmid  4268  regexmid  4278  tfisi  4328  nnregexmid  4360  iota5  4907  sbcfung  4945  funimass4  5245  dffo3  5335  eufnfv  5410  dff13  5428  ssfiexmid  6361  domfiexmid  6363  diffitest  6371  findcard  6372  findcard2  6373  findcard2s  6374  fz1sbc  9113  frecuzrdgfn  9414  bdsep2  10677  bdsepnfALT  10680  bdzfauscl  10681  bdbm1.3ii  10682  bj-2inf  10733  bj-nn0sucALT  10773  strcoll2  10778  strcollnfALT  10781