Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 2albidv | Structured version Visualization version GIF version |
Description: Formula-building rule for two universal quantifiers (deduction rule). (Contributed by NM, 4-Mar-1997.) |
Ref | Expression |
---|---|
2albidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2albidv | ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 ↔ ∀𝑥∀𝑦𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2albidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | albidv 1836 | . 2 ⊢ (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒)) |
3 | 2 | albidv 1836 | 1 ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 ↔ ∀𝑥∀𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∀wal 1473 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 |
This theorem depends on definitions: df-bi 196 |
This theorem is referenced by: dff13 6416 qliftfun 7719 seqf1o 12704 fi1uzind 13134 brfi1indALT 13137 fi1uzindOLD 13140 brfi1indALTOLD 13143 trclfvcotr 13598 dchrelbas3 24763 isch2 27464 mclsssvlem 30713 mclsval 30714 mclsax 30720 mclsind 30721 trer 31480 mbfresfi 32626 isass 32815 lpolsetN 35789 islpolN 35790 ismrc 36282 2sbc6g 37638 |
Copyright terms: Public domain | W3C validator |