![]() |
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 306 | . 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃)) |
4 | mpbir2and.3 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃))) | |
5 | 3, 4 | mpbird 167 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 |
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 7129 nqnq0pi 7439 genpassg 7527 addnqpr 7562 mulnqpr 7578 distrprg 7589 1idpr 7593 ltexpri 7614 recexprlemex 7638 aptipr 7642 cauappcvgprlemladd 7659 ltntri 8087 add20 8433 inelr 8543 recgt0 8809 prodgt0 8811 squeeze0 8863 suprzclex 9353 eluzadd 9558 eluzsub 9559 xrletrid 9807 xrre 9822 xrre3 9824 xleadd1a 9875 elioc2 9938 elico2 9939 elicc2 9940 elfz1eq 10037 fztri3or 10041 fznatpl1 10078 nn0fz0 10121 fzctr 10135 fzo1fzo0n0 10185 fzoaddel 10194 exbtwnz 10253 flid 10286 flqaddz 10299 flqdiv 10323 modqid 10351 frec2uzf1od 10408 iseqf1olemqk 10496 bcval5 10745 abs2difabs 11119 fzomaxdiflem 11123 icodiamlt 11191 dfabsmax 11228 rexico 11232 mul0inf 11251 xrbdtri 11286 sumeq2 11369 sumsnf 11419 fsum00 11472 prodeq2 11567 prodsnf 11602 zsupcllemstep 11948 zssinfcl 11951 gcd0id 11982 gcdneg 11985 nn0seqcvgd 12043 lcmval 12065 lcmneg 12076 qredeq 12098 prmind2 12122 pw2dvdseu 12170 hashdvds 12223 pcpremul 12295 pcidlem 12324 pcgcd1 12329 fldivp1 12348 pcfaclem 12349 ennnfonelemex 12417 ennnfonelemnn0 12425 mnd1 12852 grp1 12981 0subg 13064 nmznsg 13078 ring1 13241 dvdsrmuld 13270 1unit 13281 unitmulcl 13287 unitgrp 13290 unitnegcl 13304 subrguss 13362 subrgunit 13365 tgcl 13603 distop 13624 epttop 13629 neiss 13689 opnneissb 13694 ssnei2 13696 innei 13702 lmconst 13755 cnpnei 13758 cnptopco 13761 cnss1 13765 cnss2 13766 cncnpi 13767 cncnp 13769 cnconst2 13772 cnrest 13774 cnptopresti 13777 cnpdis 13781 lmtopcnp 13789 neitx 13807 tx1cn 13808 tx2cn 13809 txcnp 13810 txcnmpt 13812 txdis1cn 13817 psmetsym 13868 psmetres2 13872 isxmetd 13886 xmetsym 13907 xmetpsmet 13908 metrtri 13916 xblss2ps 13943 xblss2 13944 xblcntrps 13952 xblcntr 13953 bdxmet 14040 bdmet 14041 bdmopn 14043 xmetxp 14046 xmetxpbl 14047 rescncf 14107 cncfco 14117 mulcncflem 14129 mulcncf 14130 suplociccreex 14141 ivthinclemlopn 14153 ivthinclemuopn 14155 cnplimcim 14175 cnplimclemr 14177 limccnpcntop 14183 limccnp2cntop 14185 limccoap 14186 dvidlemap 14199 dvcn 14203 dvaddxxbr 14204 dvmulxxbr 14205 dvcoapbr 14210 dvcjbr 14211 dvrecap 14216 rpabscxpbnd 14398 lgsdirprm 14474 lgseisenlem1 14489 lgseisenlem2 14490 2sqlem8 14509 refeq 14815 apdifflemf 14833 ltlenmkv 14857 |
Copyright terms: Public domain | W3C validator |