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

Theorem syl5bir 152
 Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bir.1 (𝜓𝜑)
syl5bir.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5bir (𝜒 → (𝜑𝜃))

Proof of Theorem syl5bir
StepHypRef Expression
1 syl5bir.1 . . 3 (𝜓𝜑)
21biimpri 132 . 2 (𝜑𝜓)
3 syl5bir.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 32 1 (𝜒 → (𝜑𝜃))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ 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:  3imtr3g  203  19.37-1  1653  mo3h  2053  necon1bidc  2361  necon4aidc  2377  ceqex  2817  ssdisj  3425  ralidm  3469  exmid1dc  4132  rexxfrd  4393  sucprcreg  4473  imain  5215  f0rn0  5327  funopfv  5471  mpteqb  5521  funfvima  5659  fliftfun  5707  iinerm  6511  eroveu  6530  th3qlem1  6541  updjudhf  6977  elni2  7169  genpdisj  7378  lttri3  7891  zfz1iso  10639  cau3lem  10941  maxleast  11040  rexanre  11047  climcau  11171  summodc  11207  mertenslem2  11360  prodmodclem2  11401  prodmodc  11402  fprodseq  11407  divgcdcoprmex  11842  prmind2  11860  opnneiid  12395  txuni2  12487  txbas  12489  txbasval  12498  txlm  12510  blin2  12663  tgqioo  12778  bj-charfunr  13212
 Copyright terms: Public domain W3C validator