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 form). (Contributed by NM, 4-Mar-1997.) |
Ref | Expression |
---|---|
2albidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
2albidv | ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 ↔ ∀𝑥∀𝑦𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 2albidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | albidv 1912 | . 2 ⊢ (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒)) |
3 | 2 | albidv 1912 | 1 ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 ↔ ∀𝑥∀𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∀wal 1526 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 |
This theorem depends on definitions: df-bi 208 |
This theorem is referenced by: dff13 7004 qliftfun 8372 seqf1o 13401 fi1uzind 13845 brfi1indALT 13848 trclfvcotr 14359 dchrelbas3 25742 isch2 28928 isacycgr1 32291 mclsssvlem 32707 mclsval 32708 mclsax 32714 mclsind 32715 trer 33562 mbfresfi 34820 isass 35007 relcnveq2 35463 elrelscnveq2 35615 elsymrels3 35672 elsymrels5 35674 eltrrels3 35698 eleqvrels3 35710 lpolsetN 38500 islpolN 38501 ismrc 39178 2sbc6g 40627 fun2dmnopgexmpl 43364 |
Copyright terms: Public domain | W3C validator |