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

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

Proof of Theorem bitr4di
StepHypRef Expression
1 bitr4di.1 . 2 (𝜑 → (𝜓𝜒))
2 bitr4di.2 . . 3 (𝜃𝜒)
32bicomi 132 . 2 (𝜒𝜃)
41, 3bitrdi 196 1 (𝜑 → (𝜓𝜃))
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:  3bitr4g  223  bibi2i  227  equsalh  1726  eueq3dc  2911  sbcel12g  3072  sbceqg  3073  sbcnel12g  3074  reldisj  3474  r19.3rm  3511  eldifpr  3618  eldiftp  3637  rabxp  4659  elrng  4813  iss  4948  eliniseg  4993  fcnvres  5394  dffv3g  5506  funimass4  5561  fndmdif  5616  fneqeql  5619  funimass3  5627  elrnrexdmb  5651  dff4im  5657  fconst4m  5731  elunirn  5760  riota1  5842  riota2df  5844  f1ocnvfv3  5857  eqfnov  5974  caoftrn  6101  mpoxopovel  6235  rntpos  6251  ordgt0ge1  6429  iinerm  6600  erinxp  6602  qliftfun  6610  mapdm0  6656  elfi2  6964  fifo  6972  inl11  7057  ctssdccl  7103  isomnimap  7128  ismkvmap  7145  iswomnimap  7157  omniwomnimkv  7158  pr2nelem  7183  indpi  7319  genpdflem  7484  genpdisj  7500  genpassl  7501  genpassu  7502  ltnqpri  7571  ltpopr  7572  ltexprlemm  7577  ltexprlemdisj  7583  ltexprlemloc  7584  ltrennb  7831  letri3  8015  letr  8017  ltneg  8396  leneg  8399  reapltxor  8523  apsym  8540  suprnubex  8886  suprleubex  8887  elnnnn0  9195  zrevaddcl  9279  znnsub  9280  znn0sub  9294  prime  9328  eluz2  9510  eluz2b1  9577  nn01to3  9593  qrevaddcl  9620  xrletri3  9778  xrletr  9782  iccid  9899  elicopnf  9943  fzsplit2  10023  fzsn  10039  fzpr  10050  uzsplit  10065  fvinim0ffz  10214  lt2sqi  10580  le2sqi  10581  abs00ap  11042  iooinsup  11256  mertenslem2  11515  fprod2dlemstep  11601  gcddiv  11990  algcvgblem  12019  isprm3  12088  phisum  12210  ring1  13049  crngunit  13092  eltg2b  13187  discld  13269  opnssneib  13289  restbasg  13301  ssidcn  13343  cnptoprest2  13373  lmss  13379  txrest  13409  txlm  13412  imasnopn  13432  bldisj  13534  xmeter  13569  bl2ioo  13675  limcdifap  13764  bj-sseq  14166  nnti  14366  pw1nct  14375
  Copyright terms: Public domain W3C validator