![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbi2and | GIF version |
Description: Detach a conjunction of truths in a biconditional. (Contributed by NM, 6-Nov-2011.) (Proof shortened by Wolf Lammen, 24-Nov-2012.) |
Ref | Expression |
---|---|
mpbi2and.1 | ⊢ (𝜑 → 𝜓) |
mpbi2and.2 | ⊢ (𝜑 → 𝜒) |
mpbi2and.3 | ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃)) |
Ref | Expression |
---|---|
mpbi2and | ⊢ (𝜑 → 𝜃) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbi2and.1 | . . 3 ⊢ (𝜑 → 𝜓) | |
2 | mpbi2and.2 | . . 3 ⊢ (𝜑 → 𝜒) | |
3 | 1, 2 | jca 306 | . 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒)) |
4 | mpbi2and.3 | . 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) ↔ 𝜃)) | |
5 | 3, 4 | mpbid 147 | 1 ⊢ (𝜑 → 𝜃) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: supisoti 7040 remim 10904 resqrtcl 11073 divalgmod 11967 oddpwdclemxy 12204 divnumden 12231 numdensq 12237 prmdivdiv 12272 4sqlem7 12419 ismgmid2 12859 mnd1 12922 iscmnd 13254 imasring 13431 subrg1 13595 topgele 14006 lmcn2 14257 |
Copyright terms: Public domain | W3C validator |