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

Theorem ibar 506
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 448 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
2 simpr 462 . 2  |-  ( (
ph  /\  ps )  ->  ps )
31, 2impbid1 206 1  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  biantrur  508  biantrurd  510  anclb  549  pm5.42  550  anabs5  816  pm5.33  886  bianabs  888  baib  911  baibd  917  pclem6  938  moanim  2323  euan  2324  eueq3  3243  ifan  3952  dfopif  4178  reusv2lem5  4621  fvopab3g  5951  riota1a  6277  dfom2  6699  suppssr  6948  mpt2curryd  7015  boxcutc  7564  funisfsupp  7885  dfac3  8541  eluz2  11154  elixx3g  11637  elfz2  11778  zmodid2  12111  shftfib  13103  sadadd2lem2  14387  smumullem  14429  issubg  16761  resgrpisgrp  16782  sscntz  16924  pgrpsubgsymgbi  16992  issubrg  17936  lindsmm  19310  mdetunilem8  19568  mdetunilem9  19569  cmpsub  20339  txcnmpt  20563  fbfinnfr  20780  elfilss  20815  fixufil  20861  ibladdlem  22651  iblabslem  22659  sgmss  23893  cusgra2v  25032  eclclwwlkn1  25402  el2wlkonotot  25443  rusgranumwlklem0  25518  eupath2lem1  25547  frgra3v  25572  pjimai  27661  chrelati  27849  tltnle  28258  metidv  28531  cnambfre  31693  itg2addnclem2  31698  ibladdnclem  31702  iblabsnclem  31709  divalgmodcl  35552  expdiophlem1  35586  reuan  38005  odd2np1ALTV  38206  isrnghm  38663  rnghmval2  38666  uzlidlring  38700  islindeps  39019  elbigo2  39137
  Copyright terms: Public domain W3C validator