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 7270 genpassg 7358 addnqpr 7393 mulnqpr 7409 distrprg 7420 1idpr 7424 ltexpri 7445 recexprlemex 7469 aptipr 7473 cauappcvgprlemladd 7490 ltntri 7914 add20 8260 inelr 8370 recgt0 8632 prodgt0 8634 squeeze0 8686 suprzclex 9173 eluzadd 9378 eluzsub 9379 xrre 9633 xrre3 9635 xleadd1a 9686 elioc2 9749 elico2 9750 elicc2 9751 elfz1eq 9846 fztri3or 9850 fznatpl1 9887 nn0fz0 9930 fzctr 9941 fzo1fzo0n0 9991 fzoaddel 10000 exbtwnz 10059 flid 10088 flqaddz 10101 flqdiv 10125 modqid 10153 frec2uzf1od 10210 iseqf1olemqk 10298 bcval5 10541 abs2difabs 10912 fzomaxdiflem 10916 icodiamlt 10984 dfabsmax 11021 rexico 11025 mul0inf 11044 xrbdtri 11077 sumeq2 11160 sumsnf 11210 fsum00 11263 prodeq2 11358 zsupcllemstep 11674 zssinfcl 11677 gcd0id 11703 gcdneg 11706 nn0seqcvgd 11758 lcmval 11780 lcmneg 11791 qredeq 11813 prmind2 11837 pw2dvdseu 11882 hashdvds 11933 ennnfonelemex 11963 ennnfonelemnn0 11971 tgcl 12272 distop 12293 epttop 12298 neiss 12358 opnneissb 12363 ssnei2 12365 innei 12371 lmconst 12424 cnpnei 12427 cnptopco 12430 cnss1 12434 cnss2 12435 cncnpi 12436 cncnp 12438 cnconst2 12441 cnrest 12443 cnptopresti 12446 cnpdis 12450 lmtopcnp 12458 neitx 12476 tx1cn 12477 tx2cn 12478 txcnp 12479 txcnmpt 12481 txdis1cn 12486 psmetsym 12537 psmetres2 12541 isxmetd 12555 xmetsym 12576 xmetpsmet 12577 metrtri 12585 xblss2ps 12612 xblss2 12613 xblcntrps 12621 xblcntr 12622 bdxmet 12709 bdmet 12710 bdmopn 12712 xmetxp 12715 xmetxpbl 12716 rescncf 12776 cncfco 12786 mulcncflem 12798 mulcncf 12799 suplociccreex 12810 ivthinclemlopn 12822 ivthinclemuopn 12824 cnplimcim 12844 cnplimclemr 12846 limccnpcntop 12852 limccnp2cntop 12854 limccoap 12855 dvidlemap 12868 dvcn 12872 dvaddxxbr 12873 dvmulxxbr 12874 dvcoapbr 12879 dvcjbr 12880 dvrecap 12885 rpabscxpbnd 13067 refeq 13398 apdifflemf 13414 |
Copyright terms: Public domain | W3C validator |