![]() |
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 342 im2anan9 588 anim12dan 590 3anim123d 1298 hband 1466 hbbid 1555 spsbim 1816 moim 2064 moimv 2066 2euswapdc 2091 rspcimedv 2795 soss 4244 trin2 4938 xp11m 4985 funss 5150 fun 5303 dff13 5677 f1eqcocnv 5700 isores3 5724 isosolem 5733 f1o2ndf1 6133 tposfn2 6171 tposf1o2 6175 nndifsnid 6411 nnaordex 6431 supmoti 6888 isotilem 6901 recexprlemss1l 7467 recexprlemss1u 7468 caucvgsrlemoffres 7632 suplocsrlem 7640 nnindnn 7725 eqord1 8269 lemul12b 8643 lt2msq 8668 lbreu 8727 cju 8743 nnind 8760 uz11 9372 xrre2 9634 ico0 10070 ioc0 10071 expcan 10494 gcdaddm 11708 bezoutlemaz 11727 bezoutlembz 11728 isprm3 11835 epttop 12298 cnptopresti 12446 cnptoprest 12447 txcnp 12479 addcncntoplem 12759 mulcncflem 12798 bj-stand 13127 exmidsbthrlem 13392 |
Copyright terms: Public domain | W3C validator |