![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > jca2 | Structured version Visualization version GIF version |
Description: Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.) |
Ref | Expression |
---|---|
jca2.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
jca2.2 | ⊢ (𝜓 → 𝜃) |
Ref | Expression |
---|---|
jca2 | ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jca2.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | jca2.2 | . . 3 ⊢ (𝜓 → 𝜃) | |
3 | 2 | a1i 11 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) |
4 | 1, 3 | jcad 513 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-an 397 |
This theorem is referenced by: rr19.28v 3618 preddowncl 6284 ssimaex 6923 onfununi 8279 oaordex 8497 domtriord 9025 findcard3 9187 findcard3OLD 9188 unfilem1 9212 fodomfib 9228 inf0 9515 inf3lem3 9524 tcel 9639 fidomtri2 9888 alephval3 10004 zorn2lem6 10395 fodomb 10420 eqreznegel 12813 iserodd 16661 cshwsiun 16926 txcn 22923 ssfg 23169 fclsnei 23316 eldmgm 26317 fnrelpredd 33521 cvmlift2lem10 33734 relcnveq3 36714 iss2 36737 elrelscnveq3 36885 jca3 37250 prjspreln0 40850 omabs2 41566 rfovcnvf1od 42181 mnuop3d 42456 |
Copyright terms: Public domain | W3C validator |