![]() |
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 604 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 |
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 199 df-an 387 |
This theorem is referenced by: pm3.45 617 exdistrf 2468 2ax6elem 2583 mopick2 2720 ssrexf 3890 ssrexv 3892 ssdif 3972 ssrin 4062 reupick 4140 disjss1 4847 copsexg 5176 propeqop 5193 po3nr 5277 frss 5309 coss2 5511 ordsssuc2 6051 fununi 6197 dffv2 6518 extmptsuppeq 7583 onfununi 7704 oaass 7908 ssnnfi 8448 fiint 8506 fiss 8599 wemapsolem 8724 tcss 8897 ac6s 9621 reclem2pr 10185 qbtwnxr 12319 ico0 12509 icoshft 12585 2ffzeq 12755 clsslem 14102 r19.2uz 14468 isprm7 15791 infpn2 15988 prmgaplem4 16129 fthres2 16944 ablfacrplem 18818 monmat2matmon 20999 neiss 21284 uptx 21799 txcn 21800 nrmr0reg 21923 cnpflfi 22173 cnextcn 22241 caussi 23465 ovolsslem 23650 tgtrisegint 25811 inagswap 26148 shorth 28709 mptssALT 30022 uzssico 30093 ordtconnlem1 30515 omsmon 30905 omssubadd 30907 mclsax 32012 poseq 32292 trisegint 32674 segcon2 32751 opnrebl2 32854 poimirlem30 33983 itg2addnclem 34004 itg2addnclem2 34005 fdc1 34084 totbndss 34118 ablo4pnp 34221 keridl 34373 dib2dim 37318 dih2dimbALTN 37320 dvh1dim 37517 mapdpglem2 37748 pell14qrss1234 38264 pell1qrss14 38276 rmxycomplete 38325 lnr2i 38529 rp-fakeanorass 38700 rfcnnnub 40013 2ffzoeq 42226 nnsum4primes4 42507 nnsum4primesprm 42509 nnsum4primesgbe 42511 nnsum4primesle9 42513 |
Copyright terms: Public domain | W3C validator |