Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem imim1i 16

Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent.

Hypothesis

Ref	Expression
imim1i.1

Assertion

Ref	Expression
imim1i

---

Proof of Theorem imim1i

Step	Hyp	Ref	Expression
1		imim1i.1	. 2
2		imim1 15	. 2
3	1, 2	ax-mp 7	1

Colors of variables: wff set class

Syntax hints:   wi 3

This theorem is referenced by:  imim12i 18  syl5 21  syl7 23  pm2.86 69  loolin 72  loowoz 73  peirce 82  pm2.01 88  con2 90  imbi1i 186  dfor2 229  pm2.67 282  pm3.41 327  pm3.42 328  jaob 422  oibabs 652  pm2.26 657  dedlem0a 758  meredith 921  19.23 1059  19.39 1078  a12study 1371  r19.37av 1753  axrep1 2684  axrep2 2685  dmcosseq 3349  tz7.48lem 3940  kmlem1 4737  kmlem13 4749  axpowndlem2 4922  axacndlem4 4934  suppsr2 5195  suppsr3 5196  xrub 6027  supxrre 6030  seqzeq 6487  cau5i 6854  iserzshft2 7044  clim2serzt 7070  iserzmulc1 7072  isum1p 7141  isumreclt 7145  fsum0diaglem2 7192  islp2 7688  chcmh 9034  dmdmdt 10137  mdslmd1lem2 10161  sumdmd 10254  dmdbr6at 10256  fillsb 10435

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7

Copyright terms: Public domain