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

Theorem syl5bb 185
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bb.1 (𝜑𝜓)
syl5bb.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5bb (𝜒 → (𝜑𝜃))

Proof of Theorem syl5bb
StepHypRef Expression
1 syl5bb.1 . . 3 (𝜑𝜓)
21a1i 9 . 2 (𝜒 → (𝜑𝜓))
3 syl5bb.2 . 2 (𝜒 → (𝜓𝜃))
42, 3bitrd 181 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  syl5rbb  186  syl5bbr  187  3bitr4g  216  imim21b  245  pm5.17dc  821  dn1dc  878  bilukdc  1303  nf4dc  1576  sbal1  1894  abbi  2167  necon3abid  2259  necon3bid  2261  necon1abiidc  2280  r19.21t  2411  ceqsralt  2598  ceqsrexv  2696  ceqsrex2v  2698  elab2g  2711  elrabf  2718  eueq2dc  2736  euxfrdc  2749  eqreu  2755  reu8  2759  ru  2785  sbcralt  2861  sbcrext  2862  sbcne12g  2895  csbnestgf  2925  disjpss  3305  ralprg  3448  rexprg  3449  difsn  3528  opthpr  3570  ralunsn  3595  dfiin2g  3717  iunxsng  3759  elpwuni  3768  pwnss  3939  opelopabt  4026  opelopabga  4027  brabga  4028  elsucg  4168  elsuc2g  4169  brab2a  4420  opeliunxp  4422  posng  4439  brab2ga  4442  csbdmg  4556  elrnmpt1  4612  elrnmptg  4613  poleloe  4751  elxp4  4835  elxp5  4836  cnvpom  4887  sbcfung  4952  dffun8  4956  fncnv  4992  fununi  4994  fnssresb  5038  fnimaeq0  5047  funcocnv2  5178  dffn5im  5246  funimass4  5251  fnsnfv  5259  dmfco  5268  fndmdif  5299  fndmin  5301  unpreima  5319  respreima  5322  fsn2  5364  fnressn  5376  fressnfv  5377  elunirn  5432  dff13  5434  fliftel  5460  isoini  5484  f1oiso  5492  acexmid  5538  eloprabga  5618  resoprab2  5625  ralrnmpt2  5642  rexrnmpt2  5643  ovid  5644  ov  5647  ovg  5666  ofrfval2  5754  fmpt2x  5853  1stconst  5869  2ndconst  5870  f1od2  5883  isprmpt2  5888  brtpos2  5896  dfsmo2  5932  brdifun  6163  eqerlem  6167  brecop  6226  erovlem  6228  xpsnen  6325  xpdom2  6335  supubti  6404  ltpiord  6474  nlt1pig  6496  elinp  6629  ltdfpr  6661  genpassl  6679  genpassu  6680  1idprl  6745  1idpru  6746  gt0srpr  6890  peano2nnnn  6986  recidpirq  6991  axprecex  7011  xrlenlt  7142  addsubeq4  7288  renegcl  7334  lesub0  7547  recexaplem2  7706  conjmulap  7779  rerecclap  7780  creui  7987  peano2nn  8001  nndiv  8029  elznn0  8316  eqreznegel  8645  ltxr  8795  divelunit  8970  iccf1o  8972  elfz2  8982  elfzp1  9035  fzdifsuc  9044  fznn  9052  fzosplitsni  9192  fvinim0ffz  9197  frec2uzisod  9356  sq11i  9508  cjreb  9693  rexfiuz  9815  cau3lem  9940  divides  10109  dvdsabseq  10158  odd2np1  10183  oddm1even  10185  bj-indeq  10419  bj-nn0sucALT  10469
  Copyright terms: Public domain W3C validator