Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > anim1d | Structured version Visualization version GIF version |
Description: Add a conjunct to right of antecedent and consequent in a deduction. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
anim1d.1 | ⊢ (𝜑 → (𝜓 → 𝜒)) |
Ref | Expression |
---|---|
anim1d | ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anim1d.1 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) | |
2 | idd 24 | . 2 ⊢ (𝜑 → (𝜃 → 𝜃)) | |
3 | 1, 2 | anim12d 584 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 df-an 385 |
This theorem is referenced by: pm3.45 875 exdistrf 2321 2ax6elem 2437 mopick2 2528 ssrexf 3628 ssrexv 3630 ssdif 3707 ssrin 3800 reupick 3870 disjss1 4559 copsexg 4882 propeqop 4895 po3nr 4973 frss 5005 coss2 5200 ordsssuc2 5731 fununi 5878 dffv2 6181 extmptsuppeq 7206 onfununi 7325 oaass 7528 ssnnfi 8064 fiint 8122 fiss 8213 wemapsolem 8338 tcss 8503 ac6s 9189 reclem2pr 9749 qbtwnxr 11905 ico0 12092 icoshft 12165 2ffzeq 12329 clsslem 13571 r19.2uz 13939 isprm7 15258 infpn2 15455 prmgaplem4 15596 fthres2 16415 ablfacrplem 18287 monmat2matmon 20448 neiss 20723 uptx 21238 txcn 21239 nrmr0reg 21362 cnpflfi 21613 cnextcn 21681 caussi 22903 ovolsslem 23059 tgtrisegint 25194 inagswap 25530 cycliscrct 26158 numclwwlkovgelim 26616 shorth 27538 mptssALT 28857 ordtconlem1 29298 omsmon 29687 omssubadd 29689 mclsax 30720 poseq 30994 nodenselem5 31084 trisegint 31305 segcon2 31382 opnrebl2 31486 poimirlem30 32609 itg2addnclem 32631 itg2addnclem2 32632 fdc1 32712 totbndss 32746 ablo4pnp 32849 keridl 33001 dib2dim 35550 dih2dimbALTN 35552 dvh1dim 35749 mapdpglem2 35980 pell14qrss1234 36438 pell1qrss14 36450 rmxycomplete 36500 lnr2i 36705 rp-fakeanorass 36877 rfcnnnub 38218 nnsum4primes4 40205 nnsum4primesprm 40207 nnsum4primesgbe 40209 nnsum4primesle9 40211 2ffzoeq 40361 cyclisCrct 41005 clwwlknp 41195 |
Copyright terms: Public domain | W3C validator |