![]() |
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 295 | 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-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: anim1d 336 anim2d 337 anim12 344 im2anan9 598 anim12dan 600 3anim123d 1330 hband 1500 hbbid 1586 spsbim 1854 moim 2102 moimv 2104 2euswapdc 2129 rspcimedv 2858 soss 4329 trin2 5035 xp11m 5082 funss 5250 fun 5403 dff13 5785 f1eqcocnv 5808 isores3 5832 isosolem 5841 f1o2ndf1 6247 tposfn2 6285 tposf1o2 6289 nndifsnid 6526 nnaordex 6547 supmoti 7010 isotilem 7023 recexprlemss1l 7652 recexprlemss1u 7653 caucvgsrlemoffres 7817 suplocsrlem 7825 nnindnn 7910 eqord1 8458 lemul12b 8836 lt2msq 8861 lbreu 8920 cju 8936 nnind 8953 uz11 9568 xrre2 9839 ico0 10280 ioc0 10281 expcan 10714 gcdaddm 12003 bezoutlemaz 12022 bezoutlembz 12023 isprm3 12136 prmdiveq 12254 mulgpropdg 13070 imasabl 13234 subrgdvds 13543 epttop 13974 cnptopresti 14122 cnptoprest 14123 txcnp 14155 addcncntoplem 14435 mulcncflem 14474 bj-stand 14884 exmidsbthrlem 15155 |
Copyright terms: Public domain | W3C validator |