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

Theorem ibar 502
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 445 . 2  |-  ( ph  ->  ( ps  ->  ( ph  /\  ps ) ) )
2 simpr 459 . 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 367
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 369
This theorem is referenced by:  biantrur  504  biantrurd  506  anclb  545  pm5.42  546  anabs5  807  pm5.33  876  bianabs  878  baib  901  baibd  907  pclem6  928  cad1OLD  1469  moanim  2347  euan  2348  eueq3  3271  ifan  3975  dfopif  4200  reusv2lem5  4642  fvopab3g  5927  riota1a  6251  dfom2  6675  suppssr  6923  mpt2curryd  6990  boxcutc  7505  funisfsupp  7826  dfac3  8493  eluz2  11088  elixx3g  11545  elfz2  11682  zmodid2  12006  shftfib  12987  sadadd2lem2  14184  smumullem  14226  issubg  16400  resgrpisgrp  16421  sscntz  16563  pgrpsubgsymgbi  16631  issubrg  17624  lindsmm  19030  mdetunilem8  19288  mdetunilem9  19289  cmpsub  20067  txcnmpt  20291  fbfinnfr  20508  elfilss  20543  fixufil  20589  ibladdlem  22392  iblabslem  22400  sgmss  23578  cusgra2v  24664  eclclwwlkn1  25034  el2wlkonotot  25075  rusgranumwlklem0  25150  eupath2lem1  25179  frgra3v  25204  pjimai  27293  chrelati  27481  tltnle  27884  metidv  28106  cnambfre  30303  itg2addnclem2  30307  ibladdnclem  30311  iblabsnclem  30318  divalgmodcl  31168  expdiophlem1  31202  reuan  32424  odd2np1ALTV  32580  isrnghm  32952  rnghmval2  32955  uzlidlring  32989  islindeps  33308  elbigo2  33427
  Copyright terms: Public domain W3C validator