![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > albid | Structured version Visualization version GIF version |
Description: Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
albid.1 | ⊢ Ⅎ𝑥𝜑 |
albid.2 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
albid | ⊢ (𝜑 → (∀𝑥𝜓 ↔ ∀𝑥𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | albid.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
2 | 1 | nf5ri 2158 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) |
3 | albid.2 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 2, 3 | albidh 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 |