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  874  bianabs  876  baib  898  baibd  902  pclem6  923  cad1  1445  moanim  2345  euan  2346  euanOLD  2347  eueq3  3271  ifan  3978  dfopif  4203  reusv2lem5  4645  fvopab3g  5937  riota1a  6256  dfom2  6673  suppssr  6921  mpt2curryd  6988  boxcutc  7502  funisfsupp  7823  dfac3  8491  eluz2  11077  elixx3g  11531  elfz2  11668  zmodid2  11980  shftfib  12855  sadadd2lem2  13948  smumullem  13990  issubg  15989  resgrpisgrp  16010  sscntz  16152  pgrpsubgsymgbi  16220  issubrg  17205  lindsmm  18623  mdetunilem8  18881  mdetunilem9  18882  cmpsub  19659  txcnmpt  19853  fbfinnfr  20070  elfilss  20105  fixufil  20151  ibladdlem  21954  iblabslem  21962  sgmss  23101  cusgra2v  24124  eclclwwlkn1  24494  el2wlkonotot  24535  rusgranumwlklem0  24610  eupath2lem1  24639  frgra3v  24664  pjimai  26757  chrelati  26945  negelrp  27218  tltnle  27298  metidv  27493  cnambfre  29627  itg2addnclem2  29631  ibladdnclem  29635  iblabsnclem  29642  divalgmodcl  30522  expdiophlem1  30556  reuan  31607  islindeps  32002
  Copyright terms: Public domain W3C validator