| 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 609 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃))) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 |
| 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 207 df-an 396 |
| This theorem is referenced by: pm3.45 622 exdistrf 2452 2ax6elem 2475 mopick2 2637 ssrexf 4050 ssrexvOLD 4057 ssdif 4144 ssrin 4242 reupick 4329 disjss1 5116 copsexgw 5495 copsexg 5496 propeqop 5512 po3nr 5607 frss 5649 coss2 5867 ordsssuc2 6475 fununi 6641 dffv2 7004 oprabidw 7462 poseq 8183 extmptsuppeq 8213 onfununi 8381 oaass 8599 ssnnfi 9209 fiint 9366 fiintOLD 9367 fiss 9464 wemapsolem 9590 tcss 9784 ac6s 10524 reclem2pr 11088 qbtwnxr 13242 ico0 13433 icoshft 13513 2ffzeq 13689 clsslem 15023 r19.2uz 15390 isprm7 16745 prmdvdsncoprmbd 16764 infpn2 16951 prmgaplem4 17092 fthres2 17979 ablfacrplem 20085 rnglidlmmgm 21255 psdmul 22170 monmat2matmon 22830 neiss 23117 uptx 23633 txcn 23634 nrmr0reg 23757 cnpflfi 24007 cnextcn 24075 caussi 25331 ovolsslem 25519 tgtrisegint 28507 inagswap 28849 shorth 31314 ac6mapd 32635 mptssALT 32685 uzssico 32786 zarclsint 33871 ordtconnlem1 33923 omsmon 34300 omssubadd 34302 subgrtrl 35138 subgrcycl 35140 acycgrsubgr 35163 mclsax 35574 trisegint 36029 segcon2 36106 opnrebl2 36322 bj-19.42t 36774 poimirlem30 37657 itg2addnclem 37678 itg2addnclem2 37679 fdc1 37753 totbndss 37784 ablo4pnp 37887 keridl 38039 dib2dim 41245 dih2dimbALTN 41247 dvh1dim 41444 mapdpglem2 41675 pell14qrss1234 42867 pell1qrss14 42879 rmxycomplete 42929 lnr2i 43128 fzunt 43468 fzuntd 43469 fzunt1d 43470 fzuntgd 43471 rp-fakeanorass 43526 rfcnnnub 45041 or2expropbi 47046 2ffzoeq 47339 ich2exprop 47458 nnsum4primes4 47776 nnsum4primesprm 47778 nnsum4primesgbe 47780 nnsum4primesle9 47782 opnneir 48804 |
| Copyright terms: Public domain | W3C validator |