Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > mpbir2and | Unicode 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 7214 genpassg 7302 addnqpr 7337 mulnqpr 7353 distrprg 7364 1idpr 7368 ltexpri 7389 recexprlemex 7413 aptipr 7417 cauappcvgprlemladd 7434 ltntri 7858 add20 8204 inelr 8314 recgt0 8576 prodgt0 8578 squeeze0 8630 suprzclex 9117 eluzadd 9322 eluzsub 9323 xrre 9571 xrre3 9573 xleadd1a 9624 elioc2 9687 elico2 9688 elicc2 9689 elfz1eq 9783 fztri3or 9787 fznatpl1 9824 nn0fz0 9867 fzctr 9878 fzo1fzo0n0 9928 fzoaddel 9937 exbtwnz 9996 flid 10025 flqaddz 10038 flqdiv 10062 modqid 10090 frec2uzf1od 10147 iseqf1olemqk 10235 bcval5 10477 abs2difabs 10848 fzomaxdiflem 10852 icodiamlt 10920 dfabsmax 10957 rexico 10961 mul0inf 10980 xrbdtri 11013 sumeq2 11096 sumsnf 11146 fsum00 11199 zsupcllemstep 11565 zssinfcl 11568 gcd0id 11594 gcdneg 11597 nn0seqcvgd 11649 lcmval 11671 lcmneg 11682 qredeq 11704 prmind2 11728 pw2dvdseu 11773 hashdvds 11824 ennnfonelemex 11854 ennnfonelemnn0 11862 tgcl 12160 distop 12181 epttop 12186 neiss 12246 opnneissb 12251 ssnei2 12253 innei 12259 lmconst 12312 cnpnei 12315 cnptopco 12318 cnss1 12322 cnss2 12323 cncnpi 12324 cncnp 12326 cnconst2 12329 cnrest 12331 cnptopresti 12334 cnpdis 12338 lmtopcnp 12346 neitx 12364 tx1cn 12365 tx2cn 12366 txcnp 12367 txcnmpt 12369 txdis1cn 12374 psmetsym 12425 psmetres2 12429 isxmetd 12443 xmetsym 12464 xmetpsmet 12465 metrtri 12473 xblss2ps 12500 xblss2 12501 xblcntrps 12509 xblcntr 12510 bdxmet 12597 bdmet 12598 bdmopn 12600 xmetxp 12603 xmetxpbl 12604 rescncf 12664 cncfco 12674 mulcncflem 12686 mulcncf 12687 suplociccreex 12698 ivthinclemlopn 12710 ivthinclemuopn 12712 cnplimcim 12732 cnplimclemr 12734 limccnpcntop 12740 limccnp2cntop 12742 limccoap 12743 dvidlemap 12756 dvcn 12760 dvaddxxbr 12761 dvmulxxbr 12762 dvcoapbr 12767 dvcjbr 12768 dvrecap 12773 refeq 13150 |
Copyright terms: Public domain | W3C validator |