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 3599 preddowncl 6235 ssimaex 6853 onfununi 8172 oaordex 8389 domtriord 8910 findcard3 9057 unfilem1 9078 fodomfib 9093 inf0 9379 inf3lem3 9388 tcel 9503 fidomtri2 9752 alephval3 9866 zorn2lem6 10257 fodomb 10282 eqreznegel 12674 iserodd 16536 cshwsiun 16801 txcn 22777 ssfg 23023 fclsnei 23170 eldmgm 26171 fnrelpredd 33061 cvmlift2lem10 33274 relcnveq3 36456 iss2 36479 elrelscnveq3 36609 jca3 36870 prjspreln0 40448 rfovcnvf1od 41612 mnuop3d 41889 |
Copyright terms: Public domain | W3C validator |