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

Theorem albidv 1749
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 1462 . 2 (𝜑 → ∀𝑥𝜑)
2 albidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2albidh 1412 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wal 1285
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 1379  ax-gen 1381  ax-17 1462
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  ax11v  1752  2albidv  1792  sbal1yz  1922  eujust  1947  euf  1950  mo23  1986  axext3  2068  bm1.1  2070  eqeq1  2091  nfceqdf  2224  ralbidv2  2378  alexeq  2734  pm13.183  2745  eqeu  2776  mo2icl  2785  euind  2793  reuind  2809  cdeqal  2818  sbcal  2879  sbcalg  2880  sbcabel  2909  csbiebg  2959  ssconb  3122  reldisj  3322  sbcssg  3378  elint  3677  axsep2  3932  zfauscl  3933  bm1.3ii  3934  exmidel  4007  euotd  4054  freq1  4144  freq2  4146  eusv1  4247  ontr2exmid  4313  regexmid  4323  tfisi  4374  nnregexmid  4406  iota5  4963  sbcfung  5001  funimass4  5312  dffo3  5403  eufnfv  5480  dff13  5502  tfr1onlemsucfn  6053  tfr1onlemsucaccv  6054  tfr1onlembxssdm  6056  tfr1onlembfn  6057  tfrcllemsucfn  6066  tfrcllemsucaccv  6067  tfrcllembxssdm  6069  tfrcllembfn  6070  tfrcl  6077  frecabcl  6112  ssfiexmid  6538  domfiexmid  6540  diffitest  6549  findcard  6550  findcard2  6551  findcard2s  6552  fisseneq  6586  isomni  6729  isomnimap  6730  exmidfodomrlemr  6765  exmidfodomrlemrALT  6766  fz1sbc  9433  frecuzrdgtcl  9740  frecuzrdgfunlem  9747  zfz1iso  10135  bdsep2  11207  bdsepnfALT  11210  bdzfauscl  11211  bdbm1.3ii  11212  bj-2inf  11263  bj-nn0sucALT  11303  strcoll2  11308  strcollnfALT  11311
  Copyright terms: Public domain W3C validator