Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > jcad | GIF version |
Description: Deduction conjoining the consequents of two implications. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Jul-2013.) |
Ref | Expression |
---|---|
jcad.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
jcad.2 | ⊢ (𝜑 → (𝜓 → 𝜃)) |
Ref | Expression |
---|---|
jcad | ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | jcad.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | jcad.2 | . 2 ⊢ (𝜑 → (𝜓 → 𝜃)) | |
3 | pm3.2 138 | . 2 ⊢ (𝜒 → (𝜃 → (𝜒 ∧ 𝜃))) | |
4 | 1, 2, 3 | syl6c 66 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 107 |
This theorem is referenced by: jca2 306 jctild 314 jctird 315 ancld 323 ancrd 324 anim12ii 340 equsex 1691 equsexd 1692 rexim 2503 rr19.28v 2798 sotricim 4215 sotritrieq 4217 ordsucss 4390 ordpwsucss 4452 peano5 4482 iss 4835 funssres 5135 ssimaex 5450 elpreima 5507 resflem 5552 tposfo2 6132 nnmord 6381 map0g 6550 mapsn 6552 enq0tr 7210 addnqprl 7305 addnqpru 7306 cauappcvgprlemdisj 7427 lttri3 7812 ltleap 8362 mulgt1 8589 nominpos 8925 uzind 9130 indstr 9356 eqreznegel 9374 shftuz 10557 caucvgrelemcau 10720 sqrtsq 10784 mulcn2 11049 dvdsgcdb 11628 algcvgblem 11657 lcmdvdsb 11692 rpexp 11758 cnntr 12321 cnrest2 12332 txlm 12375 metrest 12602 bj-om 13062 |
Copyright terms: Public domain | W3C validator |