![]() |
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 306 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | mpbir2and.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | mpbird 167 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: nnnninfeq2 7140 nqnq0pi 7450 genpassg 7538 addnqpr 7573 mulnqpr 7589 distrprg 7600 1idpr 7604 ltexpri 7625 recexprlemex 7649 aptipr 7653 cauappcvgprlemladd 7670 ltntri 8098 add20 8444 inelr 8554 recgt0 8820 prodgt0 8822 squeeze0 8874 suprzclex 9364 eluzadd 9569 eluzsub 9570 xrletrid 9818 xrre 9833 xrre3 9835 xleadd1a 9886 elioc2 9949 elico2 9950 elicc2 9951 elfz1eq 10048 fztri3or 10052 fznatpl1 10089 nn0fz0 10132 fzctr 10146 fzo1fzo0n0 10196 fzoaddel 10205 exbtwnz 10264 flid 10297 flqaddz 10310 flqdiv 10334 modqid 10362 frec2uzf1od 10419 iseqf1olemqk 10507 bcval5 10756 abs2difabs 11130 fzomaxdiflem 11134 icodiamlt 11202 dfabsmax 11239 rexico 11243 mul0inf 11262 xrbdtri 11297 sumeq2 11380 sumsnf 11430 fsum00 11483 prodeq2 11578 prodsnf 11613 zsupcllemstep 11959 zssinfcl 11962 gcd0id 11993 gcdneg 11996 nn0seqcvgd 12054 lcmval 12076 lcmneg 12087 qredeq 12109 prmind2 12133 pw2dvdseu 12181 hashdvds 12234 pcpremul 12306 pcidlem 12335 pcgcd1 12340 fldivp1 12359 pcfaclem 12360 ennnfonelemex 12428 ennnfonelemnn0 12436 mnd1 12868 grp1 13002 0subg 13090 nmznsg 13104 ring1 13304 dvdsrmuld 13339 1unit 13350 unitmulcl 13356 unitgrp 13359 unitnegcl 13373 subrngintm 13427 subrguss 13451 subrgunit 13454 lsslsp 13613 tgcl 13835 distop 13856 epttop 13861 neiss 13921 opnneissb 13926 ssnei2 13928 innei 13934 lmconst 13987 cnpnei 13990 cnptopco 13993 cnss1 13997 cnss2 13998 cncnpi 13999 cncnp 14001 cnconst2 14004 cnrest 14006 cnptopresti 14009 cnpdis 14013 lmtopcnp 14021 neitx 14039 tx1cn 14040 tx2cn 14041 txcnp 14042 txcnmpt 14044 txdis1cn 14049 psmetsym 14100 psmetres2 14104 isxmetd 14118 xmetsym 14139 xmetpsmet 14140 metrtri 14148 xblss2ps 14175 xblss2 14176 xblcntrps 14184 xblcntr 14185 bdxmet 14272 bdmet 14273 bdmopn 14275 xmetxp 14278 xmetxpbl 14279 rescncf 14339 cncfco 14349 mulcncflem 14361 mulcncf 14362 suplociccreex 14373 ivthinclemlopn 14385 ivthinclemuopn 14387 cnplimcim 14407 cnplimclemr 14409 limccnpcntop 14415 limccnp2cntop 14417 limccoap 14418 dvidlemap 14431 dvcn 14435 dvaddxxbr 14436 dvmulxxbr 14437 dvcoapbr 14442 dvcjbr 14443 dvrecap 14448 rpabscxpbnd 14630 lgsdirprm 14706 lgseisenlem1 14721 lgseisenlem2 14722 2sqlem8 14741 refeq 15048 apdifflemf 15066 ltlenmkv 15090 |
Copyright terms: Public domain | W3C validator |