![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbir2and | 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 |
---|---|
mpbir2and.1 | ⊢ (𝜑 → 𝜒) |
mpbir2and.2 | ⊢ (𝜑 → 𝜃) |
mpbir2and.3 | ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) |
Ref | Expression |
---|---|
mpbir2and | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbir2and.1 | . . 3 ⊢ (𝜑 → 𝜒) | |
2 | mpbir2and.2 | . . 3 ⊢ (𝜑 → 𝜃) | |
3 | 1, 2 | jca 301 | . 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃)) |
4 | mpbir2and.3 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) | |
5 | 3, 4 | mpbird 166 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: nqnq0pi 7051 genpassg 7139 addnqpr 7174 mulnqpr 7190 distrprg 7201 1idpr 7205 ltexpri 7226 recexprlemex 7250 aptipr 7254 cauappcvgprlemladd 7271 add20 8006 inelr 8115 recgt0 8365 prodgt0 8367 squeeze0 8419 suprzclex 8898 eluzadd 9101 eluzsub 9102 xrre 9336 xrre3 9338 elioc2 9408 elico2 9409 elicc2 9410 elfz1eq 9503 fztri3or 9507 fznatpl1 9544 nn0fz0 9587 fzctr 9598 fzo1fzo0n0 9648 fzoaddel 9657 exbtwnz 9716 flid 9745 flqaddz 9758 flqdiv 9782 modqid 9810 frec2uzf1od 9867 iseqf1olemqk 9977 ibcval5 10225 abs2difabs 10595 fzomaxdiflem 10599 icodiamlt 10667 dfabsmax 10704 rexico 10708 sumeq2 10802 sumsnf 10857 fsum00 10910 zsupcllemstep 11273 zssinfcl 11276 gcd0id 11302 gcdneg 11305 nn0seqcvgd 11355 lcmval 11377 lcmneg 11388 qredeq 11410 prmind2 11434 pw2dvdseu 11478 hashdvds 11529 tgcl 11818 distop 11839 epttop 11844 rescncf 11903 cncfco 11913 |
Copyright terms: Public domain | W3C validator |