![]() |
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 607 | 1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) → (𝜒 ∧ 𝜃))) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 |
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 206 df-an 395 |
This theorem is referenced by: pm3.45 620 exdistrf 2441 2ax6elem 2464 mopick2 2626 ssrexf 4045 ssrexvOLD 4052 ssdif 4136 ssrin 4232 reupick 4318 disjss1 5116 copsexgw 5486 copsexg 5487 propeqop 5503 po3nr 5599 frss 5639 coss2 5853 ordsssuc2 6456 fununi 6623 dffv2 6986 oprabidw 7444 poseq 8161 extmptsuppeq 8191 onfununi 8360 oaass 8580 ssnnfi 9196 ssnnfiOLD 9197 fiint 9358 fiintOLD 9359 fiss 9457 wemapsolem 9583 tcss 9777 ac6s 10515 reclem2pr 11079 qbtwnxr 13224 ico0 13415 icoshft 13495 2ffzeq 13667 clsslem 14981 r19.2uz 15348 isprm7 16701 prmdvdsncoprmbd 16721 infpn2 16907 prmgaplem4 17048 fthres2 17946 ablfacrplem 20058 rnglidlmmgm 21227 psdmul 22153 monmat2matmon 22811 neiss 23098 uptx 23614 txcn 23615 nrmr0reg 23738 cnpflfi 23988 cnextcn 24056 caussi 25310 ovolsslem 25498 tgtrisegint 28420 inagswap 28762 shorth 31222 mptssALT 32589 uzssico 32686 zarclsint 33697 ordtconnlem1 33749 omsmon 34142 omssubadd 34144 subgrtrl 34971 subgrcycl 34973 acycgrsubgr 34996 mclsax 35407 trisegint 35862 segcon2 35939 opnrebl2 36043 bj-19.42t 36488 poimirlem30 37361 itg2addnclem 37382 itg2addnclem2 37383 fdc1 37457 totbndss 37488 ablo4pnp 37591 keridl 37743 dib2dim 40952 dih2dimbALTN 40954 dvh1dim 41151 mapdpglem2 41382 pell14qrss1234 42547 pell1qrss14 42559 rmxycomplete 42609 lnr2i 42811 fzunt 43156 fzuntd 43157 fzunt1d 43158 fzuntgd 43159 rp-fakeanorass 43214 rfcnnnub 44669 or2expropbi 46682 2ffzoeq 46973 ich2exprop 47076 nnsum4primes4 47394 nnsum4primesprm 47396 nnsum4primesgbe 47398 nnsum4primesle9 47400 opnneir 48273 |
Copyright terms: Public domain | W3C validator |