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

Theorem ibar 504
Description: Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.)
Assertion
Ref Expression
ibar  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )

Proof of Theorem ibar
StepHypRef Expression
1 pm3.2 447 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
2 simpr 461 . 2  |-  ( (
ph  /\  ps )  ->  ps )
31, 2impbid1 203 1  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  biantrur  506  biantrurd  508  anclb  547  pm5.42  548  anabs5  807  pm5.33  873  bianabs  875  baib  896  baibd  900  pclem6  921  cad1  1440  moanim  2330  euan  2331  euanOLD  2332  eueq3  3134  ifan  3835  dfopif  4056  reusv2lem5  4497  fvopab3g  5770  riota1a  6072  dfom2  6478  suppssr  6720  mpt2curryd  6788  boxcutc  7306  funisfsupp  7625  dfac3  8291  eluz2  10867  elixx3g  11313  elfz2  11444  zmodid2  11736  shftfib  12561  sadadd2lem2  13646  smumullem  13688  issubg  15681  resgrpisgrp  15702  sscntz  15844  pgrpsubgsymgbi  15912  issubrg  16865  lindsmm  18257  mdetunilem8  18425  mdetunilem9  18426  cmpsub  19003  txcnmpt  19197  fbfinnfr  19414  elfilss  19449  fixufil  19495  ibladdlem  21297  iblabslem  21305  sgmss  22444  cusgra2v  23370  eupath2lem1  23598  pjimai  25580  chrelati  25768  negelrp  26037  tltnle  26123  metidv  26319  cnambfre  28440  itg2addnclem2  28444  ibladdnclem  28448  iblabsnclem  28455  divalgmodcl  29336  expdiophlem1  29370  reuan  30004  el2wlkonotot  30392  eclclwwlkn1  30506  rusgranumwlklem0  30566  frgra3v  30594  islindeps  30987
  Copyright terms: Public domain W3C validator