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: nnnninfeq2 7084 nqnq0pi 7370 genpassg 7458 addnqpr 7493 mulnqpr 7509 distrprg 7520 1idpr 7524 ltexpri 7545 recexprlemex 7569 aptipr 7573 cauappcvgprlemladd 7590 ltntri 8017 add20 8363 inelr 8473 recgt0 8736 prodgt0 8738 squeeze0 8790 suprzclex 9280 eluzadd 9485 eluzsub 9486 xrletrid 9732 xrre 9747 xrre3 9749 xleadd1a 9800 elioc2 9863 elico2 9864 elicc2 9865 elfz1eq 9960 fztri3or 9964 fznatpl1 10001 nn0fz0 10044 fzctr 10058 fzo1fzo0n0 10108 fzoaddel 10117 exbtwnz 10176 flid 10209 flqaddz 10222 flqdiv 10246 modqid 10274 frec2uzf1od 10331 iseqf1olemqk 10419 bcval5 10665 abs2difabs 11036 fzomaxdiflem 11040 icodiamlt 11108 dfabsmax 11145 rexico 11149 mul0inf 11168 xrbdtri 11203 sumeq2 11286 sumsnf 11336 fsum00 11389 prodeq2 11484 prodsnf 11519 zsupcllemstep 11863 zssinfcl 11866 gcd0id 11897 gcdneg 11900 nn0seqcvgd 11952 lcmval 11974 lcmneg 11985 qredeq 12007 prmind2 12031 pw2dvdseu 12079 hashdvds 12132 pcpremul 12204 pcidlem 12233 pcgcd1 12238 fldivp1 12257 pcfaclem 12258 ennnfonelemex 12290 ennnfonelemnn0 12298 tgcl 12611 distop 12632 epttop 12637 neiss 12697 opnneissb 12702 ssnei2 12704 innei 12710 lmconst 12763 cnpnei 12766 cnptopco 12769 cnss1 12773 cnss2 12774 cncnpi 12775 cncnp 12777 cnconst2 12780 cnrest 12782 cnptopresti 12785 cnpdis 12789 lmtopcnp 12797 neitx 12815 tx1cn 12816 tx2cn 12817 txcnp 12818 txcnmpt 12820 txdis1cn 12825 psmetsym 12876 psmetres2 12880 isxmetd 12894 xmetsym 12915 xmetpsmet 12916 metrtri 12924 xblss2ps 12951 xblss2 12952 xblcntrps 12960 xblcntr 12961 bdxmet 13048 bdmet 13049 bdmopn 13051 xmetxp 13054 xmetxpbl 13055 rescncf 13115 cncfco 13125 mulcncflem 13137 mulcncf 13138 suplociccreex 13149 ivthinclemlopn 13161 ivthinclemuopn 13163 cnplimcim 13183 cnplimclemr 13185 limccnpcntop 13191 limccnp2cntop 13193 limccoap 13194 dvidlemap 13207 dvcn 13211 dvaddxxbr 13212 dvmulxxbr 13213 dvcoapbr 13218 dvcjbr 13219 dvrecap 13224 rpabscxpbnd 13406 refeq 13748 apdifflemf 13766 |
Copyright terms: Public domain | W3C validator |