![]() |
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 511 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 395 |
This theorem is referenced by: rr19.28v 3655 preddowncl 6345 ssimaex 6987 onfununi 8371 oaordex 8588 domtriord 9161 findcard3 9319 findcard3OLD 9320 unfilem1 9344 fodomfibOLD 9373 inf0 9664 inf3lem3 9673 tcel 9788 fidomtri2 10037 alephval3 10153 zorn2lem6 10544 fodomb 10569 eqreznegel 12970 iserodd 16837 cshwsiun 17102 txcn 23621 ssfg 23867 fclsnei 24014 eldmgm 27050 fnrelpredd 34926 cvmlift2lem10 35140 relcnveq3 38019 iss2 38042 elrelscnveq3 38189 jca3 38554 prjspreln0 42263 omabs2 42998 tfsconcatrn 43008 rfovcnvf1od 43671 mnuop3d 43945 |
Copyright terms: Public domain | W3C validator |