Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  albidv GIF version

Theorem albidv 1721
 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
StepHypRef Expression
1 ax-17 1435 . 2 (𝜑 → ∀𝑥𝜑)
2 albidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2albidh 1385 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 102  ∀wal 1257 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-17 1435 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  ax11v  1724  2albidv  1763  sbal1yz  1893  eujust  1918  euf  1921  mo23  1957  axext3  2039  bm1.1  2041  eqeq1  2062  nfceqdf  2193  ralbidv2  2345  alexeq  2693  pm13.183  2704  eqeu  2734  mo2icl  2743  euind  2751  reuind  2767  cdeqal  2776  sbcal  2837  sbcalg  2838  sbcabel  2867  csbiebg  2917  ssconb  3104  reldisj  3299  sbcssg  3358  elint  3649  axsep2  3904  zfauscl  3905  bm1.3ii  3906  euotd  4019  freq1  4109  freq2  4111  eusv1  4212  ontr2exmid  4278  regexmid  4288  tfisi  4338  nnregexmid  4370  iota5  4915  sbcfung  4953  funimass4  5252  dffo3  5342  eufnfv  5417  dff13  5435  ssfiexmid  6367  diffitest  6375  findcard  6376  findcard2  6377  findcard2s  6378  fz1sbc  9060  frecuzrdgfn  9362  bdsep2  10393  bdsepnfALT  10396  bdzfauscl  10397  bdbm1.3ii  10398  bj-2inf  10449  bj-nn0sucALT  10490  strcoll2  10495  strcollnfALT  10498
 Copyright terms: Public domain W3C validator