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 304 | . 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-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: nqnq0pi 7246 genpassg 7334 addnqpr 7369 mulnqpr 7385 distrprg 7396 1idpr 7400 ltexpri 7421 recexprlemex 7445 aptipr 7449 cauappcvgprlemladd 7466 ltntri 7890 add20 8236 inelr 8346 recgt0 8608 prodgt0 8610 squeeze0 8662 suprzclex 9149 eluzadd 9354 eluzsub 9355 xrre 9603 xrre3 9605 xleadd1a 9656 elioc2 9719 elico2 9720 elicc2 9721 elfz1eq 9815 fztri3or 9819 fznatpl1 9856 nn0fz0 9899 fzctr 9910 fzo1fzo0n0 9960 fzoaddel 9969 exbtwnz 10028 flid 10057 flqaddz 10070 flqdiv 10094 modqid 10122 frec2uzf1od 10179 iseqf1olemqk 10267 bcval5 10509 abs2difabs 10880 fzomaxdiflem 10884 icodiamlt 10952 dfabsmax 10989 rexico 10993 mul0inf 11012 xrbdtri 11045 sumeq2 11128 sumsnf 11178 fsum00 11231 prodeq2 11326 zsupcllemstep 11638 zssinfcl 11641 gcd0id 11667 gcdneg 11670 nn0seqcvgd 11722 lcmval 11744 lcmneg 11755 qredeq 11777 prmind2 11801 pw2dvdseu 11846 hashdvds 11897 ennnfonelemex 11927 ennnfonelemnn0 11935 tgcl 12233 distop 12254 epttop 12259 neiss 12319 opnneissb 12324 ssnei2 12326 innei 12332 lmconst 12385 cnpnei 12388 cnptopco 12391 cnss1 12395 cnss2 12396 cncnpi 12397 cncnp 12399 cnconst2 12402 cnrest 12404 cnptopresti 12407 cnpdis 12411 lmtopcnp 12419 neitx 12437 tx1cn 12438 tx2cn 12439 txcnp 12440 txcnmpt 12442 txdis1cn 12447 psmetsym 12498 psmetres2 12502 isxmetd 12516 xmetsym 12537 xmetpsmet 12538 metrtri 12546 xblss2ps 12573 xblss2 12574 xblcntrps 12582 xblcntr 12583 bdxmet 12670 bdmet 12671 bdmopn 12673 xmetxp 12676 xmetxpbl 12677 rescncf 12737 cncfco 12747 mulcncflem 12759 mulcncf 12760 suplociccreex 12771 ivthinclemlopn 12783 ivthinclemuopn 12785 cnplimcim 12805 cnplimclemr 12807 limccnpcntop 12813 limccnp2cntop 12815 limccoap 12816 dvidlemap 12829 dvcn 12833 dvaddxxbr 12834 dvmulxxbr 12835 dvcoapbr 12840 dvcjbr 12841 dvrecap 12846 refeq 13223 |
Copyright terms: Public domain | W3C validator |