ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm5.32i Unicode version

Theorem pm5.32i 442
Description: Distribution of implication over biconditional (inference rule). (Contributed by NM, 1-Aug-1994.)
Hypothesis
Ref Expression
pm5.32i.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
pm5.32i  |-  ( (
ph  /\  ps )  <->  (
ph  /\  ch )
)

Proof of Theorem pm5.32i
StepHypRef Expression
1 pm5.32i.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
2 pm5.32 441 . 2  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ( ph  /\ 
ps )  <->  ( ph  /\ 
ch ) ) )
31, 2mpbi 143 1  |-  ( (
ph  /\  ps )  <->  (
ph  /\  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  pm5.32ri  443  biadan2  444  anbi2i  445  abai  525  anabs5  538  pm5.33  574  eq2tri  2141  rexbiia  2382  reubiia  2539  rmobiia  2544  rabbiia  2592  ceqsrexbv  2727  euxfrdc  2779  eldifsn  3525  elrint  3684  elriin  3756  opeqsn  4015  rabxp  4406  eliunxp  4503  ressn  4888  fncnv  4996  dff1o5  5166  respreima  5327  dff4im  5345  dffo3  5346  f1ompt  5352  fsn  5367  fconst3m  5412  fconst4m  5413  eufnfv  5421  dff13  5439  f1mpt  5442  isores2  5484  isoini  5488  eloprabga  5622  mpt2mptx  5626  resoprab  5628  ov6g  5669  dfopab2  5846  dfoprab3s  5847  dfoprab3  5848  f1od2  5887  brtpos2  5900  dftpos3  5911  tpostpos  5913  dfsmo2  5936  xpcomco  6370  eqinfti  6492  dfplpq2  6606  dfmpq2  6607  enq0enq  6683  nqnq0a  6706  nqnq0m  6707  genpassl  6776  genpassu  6777  recexre  7745  recexgt0  7747  reapmul1  7762  apsqgt0  7768  apreim  7770  recexaplem2  7809  rerecclap  7885  elznn0  8447  elznn  8448  msqznn  8528  eluz2b1  8769  eluz2b3  8772  qreccl  8808  rpnegap  8847  elfz2nn0  9205  elfzo3  9249  frecuzrdgtcl  9494  frecuzrdgfunlem  9501  qexpclz  9594  shftidt2  9858  clim0  10262  ndvdsadd  10475  ialgfx  10578  isprm3  10644
  Copyright terms: Public domain W3C validator