![]() |
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 139 | . 2 ⊢ (𝜒 → (𝜃 → (𝜒 ∧ 𝜃))) | |
4 | 1, 2, 3 | syl6c 66 | 1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia3 108 |
This theorem is referenced by: jca2 308 jctild 316 jctird 317 ancld 325 ancrd 326 anim12ii 343 equsex 1728 equsexd 1729 rexim 2571 rr19.28v 2877 sotricim 4322 sotritrieq 4324 ordsucss 4502 ordpwsucss 4565 peano5 4596 iss 4952 funssres 5257 ssimaex 5576 elpreima 5634 resflem 5679 tposfo2 6265 nnmord 6515 map0g 6685 mapsn 6687 enq0tr 7430 addnqprl 7525 addnqpru 7526 cauappcvgprlemdisj 7647 lttri3 8033 ltleap 8585 mulgt1 8816 nominpos 9152 uzind 9360 indstr 9589 eqreznegel 9610 shftuz 10819 caucvgrelemcau 10982 sqrtsq 11046 mulcn2 11313 dvdsgcdb 12006 algcvgblem 12041 lcmdvdsb 12076 rpexp 12145 infpnlem1 12349 unitmulclb 13214 cnntr 13596 cnrest2 13607 txlm 13650 metrest 13877 bj-om 14549 |
Copyright terms: Public domain | W3C validator |