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

Theorem pm5.32i 447
Description: Distribution of implication over biconditional (inference form). (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 446 . 2  |-  ( (
ph  ->  ( ps  <->  ch )
)  <->  ( ( ph  /\ 
ps )  <->  ( ph  /\ 
ch ) ) )
31, 2mpbi 144 1  |-  ( (
ph  /\  ps )  <->  (
ph  /\  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  pm5.32ri  448  biadan2  449  anbi2i  450  abai  532  anabs5  545  pm5.33  581  eq2tri  2175  rexbiia  2425  reubiia  2590  rmobiia  2595  rabbiia  2643  ceqsrexbv  2788  euxfrdc  2841  eldifsn  3618  elrint  3779  elriin  3851  opeqsn  4142  rabxp  4544  eliunxp  4646  ressn  5047  fncnv  5157  dff1o5  5342  respreima  5514  dff4im  5532  dffo3  5533  f1ompt  5537  fsn  5558  fconst3m  5605  fconst4m  5606  eufnfv  5614  dff13  5635  f1mpt  5638  isores2  5680  isoini  5685  eloprabga  5824  mpomptx  5828  resoprab  5833  ov6g  5874  dfopab2  6053  dfoprab3s  6054  dfoprab3  6055  f1od2  6098  brtpos2  6114  dftpos3  6125  tpostpos  6127  dfsmo2  6150  elixp2  6562  mapsnen  6671  xpcomco  6686  eqinfti  6873  dfplpq2  7126  dfmpq2  7127  enq0enq  7203  nqnq0a  7226  nqnq0m  7227  genpassl  7296  genpassu  7297  axsuploc  7801  recexre  8303  recexgt0  8305  reapmul1  8320  apsqgt0  8326  apreim  8328  recexaplem2  8376  rerecclap  8453  elznn0  9023  elznn  9024  msqznn  9105  eluz2b1  9347  eluz2b3  9350  qreccl  9386  rpnegap  9425  elfz2nn0  9843  elfzo3  9891  frecuzrdgtcl  10136  frecuzrdgfunlem  10143  qexpclz  10265  shftidt2  10555  clim0  11005  iser3shft  11066  summodclem3  11100  eftlub  11306  ndvdsadd  11535  algfx  11640  isprm3  11706  ssntr  12197  tx1cn  12344  tx2cn  12345  pilem1  12766
  Copyright terms: Public domain W3C validator