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

Theorem biimtrrid 153
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
biimtrrid.1  |-  ( ps  <->  ph )
biimtrrid.2  |-  ( ch 
->  ( ps  ->  th )
)
Assertion
Ref Expression
biimtrrid  |-  ( ch 
->  ( ph  ->  th )
)

Proof of Theorem biimtrrid
StepHypRef Expression
1 biimtrrid.1 . . 3  |-  ( ps  <->  ph )
21biimpri 133 . 2  |-  ( ph  ->  ps )
3 biimtrrid.2 . 2  |-  ( ch 
->  ( ps  ->  th )
)
42, 3syl5 32 1  |-  ( ch 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> 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:  3imtr3g  204  19.37-1  1674  mo3h  2079  necon1bidc  2399  necon4aidc  2415  r19.30dc  2624  ceqex  2864  ssdisj  3479  ralidm  3523  exmid1dc  4200  rexxfrd  4463  sucprcreg  4548  imain  5298  f0rn0  5410  funopfv  5555  mpteqb  5606  funfvima  5748  fliftfun  5796  iinerm  6606  eroveu  6625  th3qlem1  6636  updjudhf  7077  elni2  7312  genpdisj  7521  lttri3  8035  nn0ltexp2  10685  zfz1iso  10816  cau3lem  11118  maxleast  11217  rexanre  11224  climcau  11350  summodc  11386  mertenslem2  11539  prodmodclem2  11580  prodmodc  11581  fprodseq  11586  divgcdcoprmex  12096  prmind2  12114  pcqmul  12297  pcxcl  12305  pcadd  12333  mul4sq  12386  issubg2m  13002  dvdsrtr  13223  unitgrp  13238  subrgintm  13324  opnneiid  13557  txuni2  13649  txbas  13651  txbasval  13660  txlm  13672  blin2  13825  tgqioo  13940  2sqlem5  14348  bj-charfunr  14444
  Copyright terms: Public domain W3C validator