|   | 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 1920 | . 2 ⊢ (𝜑 → (∀𝑦𝜓 ↔ ∀𝑦𝜒)) | 
| 3 | 2 | albidv 1920 | 1 ⊢ (𝜑 → (∀𝑥∀𝑦𝜓 ↔ ∀𝑥∀𝑦𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 | 
| This theorem depends on definitions: df-bi 207 | 
| This theorem is referenced by: dff13 7275 xpord2indlem 8172 xpord3inddlem 8179 qliftfun 8842 seqf1o 14084 fi1uzind 14546 brfi1indALT 14549 trclfvcotr 15048 dchrelbas3 27282 isch2 31242 isacycgr1 35151 mclsssvlem 35567 mclsval 35568 mclsax 35574 mclsind 35575 trer 36317 mbfresfi 37673 isass 37853 relcnveq2 38324 elrelscnveq2 38494 elsymrels3 38555 elsymrels5 38557 eltrrels3 38581 eleqvrels3 38594 lpolsetN 41484 islpolN 41485 ismrc 42712 2sbc6g 44434 fun2dmnopgexmpl 47296 joindm2 48865 meetdm2 48867 | 
| Copyright terms: Public domain | W3C validator |