![]() |
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 587 | 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 197 df-an 385 |
This theorem is referenced by: pm3.45 915 exdistrf 2473 2ax6elem 2586 mopick2 2678 ssrexf 3806 ssrexv 3808 ssdif 3888 ssrin 3981 reupick 4054 disjss1 4778 copsexg 5104 propeqop 5118 po3nr 5201 frss 5233 coss2 5434 ordsssuc2 5975 fununi 6125 dffv2 6433 extmptsuppeq 7487 onfununi 7607 oaass 7810 ssnnfi 8344 fiint 8402 fiss 8495 wemapsolem 8620 tcss 8793 ac6s 9498 reclem2pr 10062 qbtwnxr 12224 ico0 12414 icoshft 12487 2ffzeq 12654 clsslem 13924 r19.2uz 14290 isprm7 15622 infpn2 15819 prmgaplem4 15960 fthres2 16793 ablfacrplem 18664 monmat2matmon 20831 neiss 21115 uptx 21630 txcn 21631 nrmr0reg 21754 cnpflfi 22004 cnextcn 22072 caussi 23295 ovolsslem 23452 tgtrisegint 25593 inagswap 25929 shorth 28463 mptssALT 29783 uzssico 29855 ordtconnlem1 30279 omsmon 30669 omssubadd 30671 mclsax 31773 poseq 32059 trisegint 32441 segcon2 32518 opnrebl2 32622 poimirlem30 33752 itg2addnclem 33774 itg2addnclem2 33775 fdc1 33855 totbndss 33889 ablo4pnp 33992 keridl 34144 dib2dim 37034 dih2dimbALTN 37036 dvh1dim 37233 mapdpglem2 37464 pell14qrss1234 37922 pell1qrss14 37934 rmxycomplete 37984 lnr2i 38188 rp-fakeanorass 38360 rfcnnnub 39694 2ffzoeq 41848 nnsum4primes4 42187 nnsum4primesprm 42189 nnsum4primesgbe 42191 nnsum4primesle9 42193 |
Copyright terms: Public domain | W3C validator |