![]() |
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 3623 preddowncl 6291 ssimaex 6931 onfununi 8292 oaordex 8510 domtriord 9074 findcard3 9236 findcard3OLD 9237 unfilem1 9261 fodomfib 9277 inf0 9566 inf3lem3 9575 tcel 9690 fidomtri2 9939 alephval3 10055 zorn2lem6 10446 fodomb 10471 eqreznegel 12868 iserodd 16718 cshwsiun 16983 txcn 23014 ssfg 23260 fclsnei 23407 eldmgm 26408 fnrelpredd 33782 cvmlift2lem10 33993 relcnveq3 36855 iss2 36878 elrelscnveq3 37026 jca3 37391 prjspreln0 41005 omabs2 41725 tfsconcatrn 41735 rfovcnvf1od 42398 mnuop3d 42673 |
Copyright terms: Public domain | W3C validator |