MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imbi1i Unicode version

Theorem imbi1i 315
Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
Hypothesis
Ref Expression
imbi1i.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
imbi1i  |-  ( (
ph  ->  ch )  <->  ( ps  ->  ch ) )

Proof of Theorem imbi1i
StepHypRef Expression
1 imbi1i.1 . 2  |-  ( ph  <->  ps )
2 imbi1 313 . 2  |-  ( (
ph 
<->  ps )  ->  (
( ph  ->  ch )  <->  ( ps  ->  ch )
) )
31, 2ax-mp 8 1  |-  ( (
ph  ->  ch )  <->  ( ps  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  imbi12i  316  imor  401  ancomsimp  1360  19.43  1596  19.37  1840  dfsb3  2028  sbor  2038  sbrim  2039  mo4f  2208  2mos  2255  neor  2563  r3al  2634  r19.23t  2691  r19.43  2729  ceqsralt  2845  ralab  2960  ralrab  2961  euind  2986  reu2  2987  rmo4  2992  reuind  3002  2reu5lem3  3006  rmo3  3112  unss  3383  ralunb  3390  inssdif0  3555  ssundif  3571  dfif2  3601  pwss  3673  ralsns  3704  disjsn  3727  snss  3782  unissb  3894  intun  3931  intpr  3932  dfiin2g  3973  disjor  4044  dftr2  4152  axrep1  4169  axpweq  4224  zfpow  4226  axpow2  4227  zfun  4550  uniex2  4552  reusv2lem4  4575  reusv2  4577  reusv7OLD  4583  dfom2  4695  raliunxp  4862  asymref2  5097  dffun2  5302  dffun4  5304  dffun5  5305  dffun7  5317  fununi  5353  dff13  5825  fimaxg  7149  fiint  7178  dfsup2  7240  oemapso  7429  scottexs  7602  scott0s  7603  iscard2  7654  acnnum  7724  dfac9  7807  dfacacn  7812  kmlem4  7824  kmlem12  7832  axpowndlem3  8266  zfcndun  8282  zfcndpow  8283  zfcndac  8286  axgroth5  8491  grothpw  8493  axgroth6  8495  infm3  9758  raluz2  10315  nnwos  10333  ralrp  10419  lo1resb  12085  rlimresb  12086  o1resb  12087  isprm4  12815  acsfn1  13612  acsfn2  13614  lubid  14165  isirred2  15532  isdomn2  16089  iunocv  16637  ist1-2  17131  isnrm2  17142  dfcon2  17201  alexsubALTlem3  17795  ismbl  18938  dyadmbllem  19007  ellimc3  19282  dchrelbas2  20529  dchrelbas3  20530  isch2  21858  choc0  21960  h1dei  22184  mdsl2i  22957  xfree2  23080  rmo3f  23118  rmo4fOLD  23119  rmo4f  23120  disjorf  23164  esumpcvgval  23644  esumcvg  23652  axextprim  24331  axunprim  24333  axpowprim  24334  untuni  24339  3orit  24350  biimpexp  24354  dfon2lem8  24531  predreseq  24564  soseq  24639  dfom5b  24837  raldifsni  25901  fphpd  26047  dford4  26270  fnwe2lem2  26296  islindf4  26456  isdomn3  26671  pm14.12  26769  dfvd2an  27845  dfvd3  27854  dfvd3an  27857  uun2221  28097  uun2221p1  28098  uun2221p2  28099  bnj538  28280  bnj1101  28327  bnj1109  28329  bnj1533  28395  bnj580  28456  bnj864  28465  bnj865  28466  bnj978  28492  bnj1049  28515  bnj1090  28520  bnj1145  28534  sborNEW7  28736  sbrimNEW7  28737  dfsb3NEW7  28806  a12study8  28937  a12study9  28938  a12peros  28939  a12lem2  28949  cvlsupr3  29352  pmapglbx  29776  isltrn2N  30127  cdleme0moN  30232  cdlemefrs29bpre0  30403
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177
  Copyright terms: Public domain W3C validator