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

Theorem ibar 491
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 435 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
2 simpr 448 . 2  |-  ( (
ph  /\  ps )  ->  ps )
31, 2impbid1 195 1  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359
This theorem is referenced by:  biantrur  493  biantrurd  495  anclb  531  pm5.42  532  anabs5  785  pm5.33  849  bianabs  851  baib  872  baibd  876  pclem6  897  cad1  1407  euan  2337  eueq3  3101  ifan  3770  dfopif  3973  reusv2lem5  4720  dfom2  4839  fvopab3g  5794  riota1a  6561  boxcutc  7097  dfac3  7994  eluz2  10486  elixx3g  10921  elfz2  11042  shftfib  11879  sadadd2lem2  12954  smumullem  12996  issubg  14936  sscntz  15117  issubrg  15860  cmpsub  17455  txcnmpt  17648  fbfinnfr  17865  elfilss  17900  fixufil  17946  ibladdlem  19703  iblabslem  19711  sgmss  20881  cusgra2v  21463  eupath2lem1  21691  pjimai  23671  chrelati  23859  tltnle  24182  metidv  24279  zmodid2  25106  wl-pm5.32  26221  cnambfre  26245  itg2addnclem2  26247  ibladdnclem  26251  iblabsnclem  26258  divalgmodcl  27049  expdiophlem1  27083  lindsmm  27266  reuan  27925  el2wlkonotot  28293  frgra3v  28329
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 178  df-an 361
  Copyright terms: Public domain W3C validator