Theorem pm5.32i 454

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

Step	Hyp	Ref	Expression
1		pm5.32i.1	. 2 |- ( ph -> ( ps <-> ch ) )
2		pm5.32 453	. 2 |- ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph /\ ps ) <-> ( ph /\ ch ) ) )
3	1, 2	mpbi 145	1 |- ( ( ph /\ ps ) <-> ( ph /\ ch ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm5.32ri  455  biadan2  456  anbi2i  457  abai  560  anabs5  573  pm5.33  609  eq2tri  2264  rexbiia  2520  reubiia  2690  rmobiia  2695  rabbiia  2756  ceqsrexbv  2903  euxfrdc  2958  eldifpr  3659  eldiftp  3678  eldifsn  3759  elrint  3924  elriin  3997  opeqsn  4296  rabxp  4711  eliunxp  4816  restidsing  5014  ressn  5222  fncnv  5339  dff1o5  5530  respreima  5707  dff4im  5725  dffo3  5726  f1ompt  5730  fsn  5751  fconst3m  5802  fconst4m  5803  eufnfv  5814  dff13  5836  f1mpt  5839  isores2  5881  isoini  5886  eloprabga  6031  mpomptx  6035  resoprab  6040  ov6g  6083  dfopab2  6274  dfoprab3s  6275  dfoprab3  6276  f1od2  6320  brtpos2  6336  dftpos3  6347  tpostpos  6349  dfsmo2  6372  elixp2  6788  mapsnen  6902  xpcomco  6920  eqinfti  7121  dfplpq2  7466  dfmpq2  7467  enq0enq  7543  nqnq0a  7566  nqnq0m  7567  genpassl  7636  genpassu  7637  axsuploc  8144  recexre  8650  recexgt0  8652  reapmul1  8667  apsqgt0  8673  apreim  8675  recexaplem2  8724  rerecclap  8802  elznn0  9386  elznn  9387  msqznn  9472  eluz2b1  9721  eluz2b3  9724  qreccl  9762  rpnegap  9807  elfz2nn0  10233  elfzo3  10285  frecuzrdgtcl  10555  frecuzrdgfunlem  10562  qexpclz  10703  shftidt2  11114  clim0  11567  iser3shft  11628  summodclem3  11662  fprod2dlemstep  11904  eftlub  11972  ndvdsadd  12213  algfx  12345  isprm3  12411  isprm5  12435  xpsfrnel  13147  isabl2  13601  dvdsrcl2  13832  unitinvcl  13856  unitinvinv  13857  unitlinv  13859  unitrinv  13860  isrim  13902  isnzr2  13917  islmod  14024  isridl  14237  cnfldui  14322  ssntr  14565  tx1cn  14712  tx2cn  14713  pilem1  15222  lgsdir2lem4  15479