![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > anim1ci | Structured version Visualization version GIF version |
Description: Introduce conjunct to both sides of an implication. (Contributed by Peter Mazsa, 24-Sep-2022.) |
Ref | Expression |
---|---|
anim1i.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
anim1ci | ⊢ ((𝜑 ∧ 𝜒) → (𝜒 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | anim1i.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | id 22 | . 2 ⊢ (𝜒 → 𝜒) | |
3 | 1, 2 | anim12ci 607 | 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: elpwdifsn 4552 f1ocnv 6403 frnssb 6655 dfrecs3 7752 odi 7943 snmapen 8322 infcntss 8522 lediv2a 11271 lbreu 11327 nn2ge 11403 dfceil2 12959 leexp1a 13237 faclbnd6 13404 ccatval3 13669 ccatalpha 13683 ccatpfx 13810 pfxccatin12lem2 13858 pfxccat3 13863 pfxccat3a 13869 repsdf2 13924 repswsymball 13925 dvdsdivcl 15445 nn0ehalf 15508 nn0oddm1d2 15515 nnoddm1d2 15516 sumeven 15517 ndvdssub 15539 coprmgcdb 15768 ncoprmgcdne1b 15769 divgcdcoprm0 15784 ncoprmlnprm 15840 vfermltl 15910 powm2modprm 15912 modprmn0modprm0 15916 dvdsprmpweqle 15994 prmgaplem4 16162 prmgaplem7 16165 cshwshashlem2 16202 logbgcd1irr 24972 wlkreslem 27018 wwlksnextbi 27255 hhcmpl 28629 elbigolo1 43348 2sphere 43467 itsclquadb 43494 |
Copyright terms: Public domain | W3C validator |