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

Theorem albidv 1811
Description: Formula-building rule for universal quantifier (deduction form). (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 1513 . 2 (𝜑 → ∀𝑥𝜑)
2 albidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2albidh 1467 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wal 1340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-17 1513
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ax11v  1814  2albidv  1854  sbal1yz  1988  eujust  2015  euf  2018  mo23  2054  axext3  2147  bm1.1  2149  eqeq1  2171  cbvabw  2287  nfceqdf  2305  ralbidv2  2466  alexeq  2850  pm13.183  2862  eqeu  2894  mo2icl  2903  euind  2911  reuind  2929  cdeqal  2938  sbcal  3000  sbcalg  3001  sbcabel  3030  csbcow  3054  csbiebg  3085  ssconb  3253  reldisj  3458  sbcssg  3516  elint  3827  axsep2  4098  zfauscl  4099  bm1.3ii  4100  exmidel  4181  euotd  4229  freq1  4319  freq2  4321  eusv1  4427  ontr2exmid  4499  regexmid  4509  tfisi  4561  nnregexmid  4595  iota5  5170  sbcfung  5209  funimass4  5534  dffo3  5629  eufnfv  5712  dff13  5733  tfr1onlemsucfn  6302  tfr1onlemsucaccv  6303  tfr1onlembxssdm  6305  tfr1onlembfn  6306  tfrcllemsucfn  6315  tfrcllemsucaccv  6316  tfrcllembxssdm  6318  tfrcllembfn  6319  tfrcl  6326  frecabcl  6361  ssfiexmid  6836  domfiexmid  6838  diffitest  6847  findcard  6848  findcard2  6849  findcard2s  6850  fiintim  6888  fisseneq  6891  isomni  7094  isomnimap  7095  ismkv  7111  ismkvmap  7112  iswomni  7123  iswomnimap  7124  omniwomnimkv  7125  exmidfodomrlemr  7152  exmidfodomrlemrALT  7153  fz1sbc  10025  frecuzrdgtcl  10341  frecuzrdgfunlem  10348  zfz1iso  10748  istopg  12595  bdsep2  13661  bdsepnfALT  13664  bdzfauscl  13665  bdbm1.3ii  13666  bj-2inf  13713  bj-nn0sucALT  13753  sscoll2  13763
  Copyright terms: Public domain W3C validator