![]() |
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 302 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | mpbir2and.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | mpbird 166 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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 7147 genpassg 7235 addnqpr 7270 mulnqpr 7286 distrprg 7297 1idpr 7301 ltexpri 7322 recexprlemex 7346 aptipr 7350 cauappcvgprlemladd 7367 ltntri 7761 add20 8103 inelr 8212 recgt0 8466 prodgt0 8468 squeeze0 8520 suprzclex 9001 eluzadd 9204 eluzsub 9205 xrre 9444 xrre3 9446 xleadd1a 9497 elioc2 9560 elico2 9561 elicc2 9562 elfz1eq 9656 fztri3or 9660 fznatpl1 9697 nn0fz0 9740 fzctr 9751 fzo1fzo0n0 9801 fzoaddel 9810 exbtwnz 9869 flid 9898 flqaddz 9911 flqdiv 9935 modqid 9963 frec2uzf1od 10020 iseqf1olemqk 10108 bcval5 10350 abs2difabs 10720 fzomaxdiflem 10724 icodiamlt 10792 dfabsmax 10829 rexico 10833 mul0inf 10851 xrbdtri 10884 sumeq2 10967 sumsnf 11017 fsum00 11070 zsupcllemstep 11433 zssinfcl 11436 gcd0id 11462 gcdneg 11465 nn0seqcvgd 11515 lcmval 11537 lcmneg 11548 qredeq 11570 prmind2 11594 pw2dvdseu 11638 hashdvds 11689 ennnfonelemex 11719 ennnfonelemnn0 11727 tgcl 12015 distop 12036 epttop 12041 neiss 12101 opnneissb 12106 ssnei2 12108 innei 12114 lmconst 12166 cnpnei 12169 cnptopco 12172 cnss1 12176 cnss2 12177 cncnpi 12178 cncnp 12180 cnconst2 12183 cnrest 12185 cnptopresti 12188 cnpdis 12192 lmtopcnp 12200 neitx 12218 tx1cn 12219 tx2cn 12220 txcnp 12221 txcnmpt 12223 txdis1cn 12228 psmetsym 12257 psmetres2 12261 isxmetd 12275 xmetsym 12296 xmetpsmet 12297 metrtri 12305 xblss2ps 12332 xblss2 12333 xblcntrps 12341 xblcntr 12342 bdxmet 12429 bdmet 12430 bdmopn 12432 rescncf 12481 cncfco 12491 mulcncflem 12502 mulcncf 12503 cnplimcim 12516 limccnpcntop 12520 dvidlemap 12533 refeq 12807 |
Copyright terms: Public domain | W3C validator |