![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > mpbir3and | GIF version |
Description: Detach a conjunction of truths in a biconditional. (Contributed by Mario Carneiro, 11-May-2014.) |
Ref | Expression |
---|---|
mpbir3and.1 | ⊢ (𝜑 → 𝜒) |
mpbir3and.2 | ⊢ (𝜑 → 𝜃) |
mpbir3and.3 | ⊢ (𝜑 → 𝜏) |
mpbir3and.4 | ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) |
Ref | Expression |
---|---|
mpbir3and | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpbir3and.1 | . . 3 ⊢ (𝜑 → 𝜒) | |
2 | mpbir3and.2 | . . 3 ⊢ (𝜑 → 𝜃) | |
3 | mpbir3and.3 | . . 3 ⊢ (𝜑 → 𝜏) | |
4 | 1, 2, 3 | 3jca 1179 | . 2 ⊢ (𝜑 → (𝜒 ∧ 𝜃 ∧ 𝜏)) |
5 | mpbir3and.4 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜒 ∧ 𝜃 ∧ 𝜏))) | |
6 | 4, 5 | mpbird 167 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 ∧ w3a 980 |
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 df-3an 982 |
This theorem is referenced by: ixxss1 9922 ixxss2 9923 ixxss12 9924 ubioc1 9947 lbico1 9948 lbicc2 10002 ubicc2 10003 elicod 10283 modqelico 10352 zmodfz 10364 modqmuladdim 10385 addmodid 10390 phicl2 12232 isstruct2r 12491 issubmd 12892 mndissubm 12893 submid 12895 subsubm 12901 0subm 12902 mhmima 12909 mhmeql 12910 issubgrpd2 13095 grpissubg 13099 subgintm 13103 nmzsubg 13115 eqger 13129 eqgcpbl 13133 ghmrn 13157 ghmpreima 13166 unitsubm 13430 subrgsubm 13542 subrgugrp 13548 subrgintm 13551 islssmd 13636 lsssubg 13654 islss4 13659 issubrgd 13729 lidlsubg 13763 2idlcpblrng 13799 lmtopcnp 14147 xmeter 14333 tgqioo 14444 suplociccreex 14499 dedekindicc 14508 ivthinclemlopn 14511 ivthinclemuopn 14513 sin0pilem2 14600 pilem3 14601 coseq0q4123 14652 |
Copyright terms: Public domain | W3C validator |