![]() |
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 290 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜏))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: anim1d 330 anim2d 331 prth 337 im2anan9 566 anim12dan 568 3anim123d 1256 hband 1424 hbbid 1513 spsbim 1772 moim 2013 moimv 2015 2euswapdc 2040 rspcimedv 2725 soss 4150 trin2 4836 xp11m 4882 funss 5047 fun 5196 dff13 5561 f1eqcocnv 5584 isores3 5608 isosolem 5617 f1o2ndf1 6007 tposfn2 6045 tposf1o2 6049 nndifsnid 6280 nnaordex 6300 supmoti 6742 isotilem 6755 recexprlemss1l 7255 recexprlemss1u 7256 caucvgsrlemoffres 7406 nnindnn 7489 eqord1 8022 lemul12b 8383 lt2msq 8408 lbreu 8467 cju 8482 nnind 8499 uz11 9102 xrre2 9344 ico0 9734 ioc0 9735 expcan 10186 gcdaddm 11314 bezoutlemaz 11331 bezoutlembz 11332 isprm3 11439 epttop 11851 exmidsbthrlem 12184 |
Copyright terms: Public domain | W3C validator |