![]() |
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 1924 | . 2 ⊢ (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒)) |
3 | 2 | albidv 1924 | 1 ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 ↔ ∀𝑥∀𝑦𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 |
This theorem depends on definitions: df-bi 206 |
This theorem is referenced by: dff13 7248 xpord2indlem 8127 xpord3inddlem 8134 qliftfun 8791 seqf1o 14004 fi1uzind 14453 brfi1indALT 14456 trclfvcotr 14951 dchrelbas3 26720 isch2 30453 isacycgr1 34074 mclsssvlem 34490 mclsval 34491 mclsax 34497 mclsind 34498 trer 35138 mbfresfi 36471 isass 36651 relcnveq2 37129 elrelscnveq2 37300 elsymrels3 37361 elsymrels5 37363 eltrrels3 37387 eleqvrels3 37400 lpolsetN 40290 islpolN 40291 ismrc 41371 2sbc6g 43106 fun2dmnopgexmpl 45926 joindm2 47502 meetdm2 47504 |
Copyright terms: Public domain | W3C validator |