Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > anim12d | GIF version |
Description: Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.) |
Ref | Expression |
---|---|
anim12d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
anim12d.2 | ⊢ (𝜑 → (𝜃 → 𝜏)) |
Ref | Expression |
---|---|
anim12d | ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anim12d.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | anim12d.2 | . 2 ⊢ (𝜑 → (𝜃 → 𝜏)) | |
3 | idd 21 | . 2 ⊢ (𝜑 → ((𝜒 ∧ 𝜏) → (𝜒 ∧ 𝜏))) | |
4 | 1, 2, 3 | syl2and 293 | 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-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: anim1d 334 anim2d 335 anim12 341 im2anan9 587 anim12dan 589 3anim123d 1297 hband 1465 hbbid 1554 spsbim 1815 moim 2061 moimv 2063 2euswapdc 2088 rspcimedv 2786 soss 4231 trin2 4925 xp11m 4972 funss 5137 fun 5290 dff13 5662 f1eqcocnv 5685 isores3 5709 isosolem 5718 f1o2ndf1 6118 tposfn2 6156 tposf1o2 6160 nndifsnid 6396 nnaordex 6416 supmoti 6873 isotilem 6886 recexprlemss1l 7436 recexprlemss1u 7437 caucvgsrlemoffres 7601 suplocsrlem 7609 nnindnn 7694 eqord1 8238 lemul12b 8612 lt2msq 8637 lbreu 8696 cju 8712 nnind 8729 uz11 9341 xrre2 9597 ico0 10032 ioc0 10033 expcan 10456 gcdaddm 11661 bezoutlemaz 11680 bezoutlembz 11681 isprm3 11788 epttop 12248 cnptopresti 12396 cnptoprest 12397 txcnp 12429 addcncntoplem 12709 mulcncflem 12748 bj-stand 12945 exmidsbthrlem 13206 |
Copyright terms: Public domain | W3C validator |