![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 2albii | GIF version |
Description: Inference adding 2 universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.) |
Ref | Expression |
---|---|
albii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
2albii | ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | albii.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
2 | 1 | albii 1404 | . 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓) |
3 | 2 | albii 1404 | 1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 103 ∀wal 1287 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-gen 1383 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: mor 1990 mo4f 2008 moanim 2022 2eu4 2041 ralcomf 2528 raliunxp 4577 cnvsym 4815 intasym 4816 intirr 4818 codir 4820 qfto 4821 dffun4 5026 dffun4f 5031 funcnveq 5077 fun11 5081 fununi 5082 mpt22eqb 5754 addnq0mo 7006 mulnq0mo 7007 addsrmo 7289 mulsrmo 7290 |
Copyright terms: Public domain | W3C validator |