MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  albid Structured version   Visualization version   GIF version

Theorem albid 2188
Description: Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypotheses
Ref Expression
albid.1 𝑥𝜑
albid.2 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
albid (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))

Proof of Theorem albid
StepHypRef Expression
1 albid.1 . . 3 𝑥𝜑
21nf5ri 2158 . 2 (𝜑 → ∀𝑥𝜑)
3 albid.2 . 2 (𝜑 → (𝜓𝜒))
42, 3albidh 1849 1 (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wal 1520  wnf 1766
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-12 2140
This theorem depends on definitions:  df-bi 208  df-ex 1763  df-nf 1767
This theorem is referenced by:  nfbidf  2190  axc15OLD  2400  dral2  2416  dral1  2417  sb4b  2456  sbal1  2524  sbal2  2525  sbal2OLD  2526  sbal2OLDOLD  2527  mobidOLD  2589  ralbida  3193  raleqf  3356  intab  4814  fin23lem32  9615  axrepndlem1  9863  axrepndlem2  9864  axrepnd  9865  axunnd  9867  axpowndlem2  9869  axpowndlem4  9871  axregndlem2  9874  axinfndlem1  9876  axinfnd  9877  axacndlem4  9881  axacndlem5  9882  axacnd  9883  iota5f  32557  bj-dral1v  33677  exrecfnlem  34204  wl-equsald  34324  wl-sbnf1  34335  wl-2sb6d  34338  wl-sbalnae  34342  wl-mo2df  34350  wl-eudf  34352  wl-ax11-lem6  34366  wl-ax11-lem8  34368  wl-dfrmof  34399  ax12eq  35621  ax12el  35622  ax12v2-o  35629
  Copyright terms: Public domain W3C validator