MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimtrrid Structured version   Visualization version   GIF version

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

Proof of Theorem biimtrrid
StepHypRef Expression
1 biimtrrid.1 . . 3 (𝜓𝜑)
21biimpri 227 . 2 (𝜑𝜓)
3 biimtrrid.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5 34 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206
This theorem is referenced by:  3imtr3g  295  oplem1  1056  nic-ax  1676  19.30  1885  19.33b  1889  necon1bd  2960  spc2d  3560  pssdifn0  4324  ralnralall  4475  disjss3  5103  somo  5581  frminex  5612  sofld  6138  predtrss  6275  ordelord  6338  unizlim  6438  f0rn0  6725  funopfv  6892  mpteqb  6965  fvrnressn  7104  funfvima  7177  fpropnf1  7211  fliftfun  7254  weniso  7296  tfinds  7789  tfindsg  7790  tfindes  7792  tfinds2  7793  findsg  7829  frxp  8051  poxp2  8068  soseq  8084  suppssr  8120  rdgsucmptnf  8368  frsucmptn  8378  tz7.49  8384  om00  8515  oewordi  8531  iiner  8687  eroveu  8710  fsetexb  8761  undomOLD  8963  sucdom2OLD  8985  sdomdif  9028  pssnn  9071  sucdom2  9109  php3  9115  php3OLD  9127  unxpdomlem3  9155  fisseneq  9160  pssnnOLD  9168  ordunifi  9196  isfinite2  9204  fiint  9227  infssuni  9246  ixpfi2  9253  finsschain  9262  ordtypelem10  9422  wofib  9440  wemapsolem  9445  unxpwdom2  9483  inf3lem2  9524  cantnfp1lem3  9575  cantnfp1  9576  setind  9629  frr3g  9651  r1tr  9671  r1ordg  9673  rankelb  9719  rankxplim3  9776  updjudhf  9826  cardlim  9867  infxpenlem  9908  infxpenc2  9917  dfac5lem4  10021  dfac12k  10042  kmlem13  10057  sornom  10172  fin23lem25  10219  fin23lem21  10234  zorn2lem4  10394  iundom2g  10435  fpwwe2lem11  10536  fpwwe2lem12  10537  pwfseqlem4a  10556  eltsk2g  10646  inttsk  10669  tskord  10675  r1tskina  10677  grudomon  10712  arch  12369  zaddcl  12502  uzm1  12756  xrsupsslem  13181  xrinfmsslem  13182  fsequb  13835  fseqsupubi  13838  ssnn0fi  13845  seqf1o  13904  sq01  14080  ccatalpha  14435  swrdnd0  14503  repsdf2  14624  cshw1  14668  wrdl3s3  14811  rexanre  15191  rexuzre  15197  cau3lem  15199  o1co  15428  rlimcn3  15432  o1of2  15455  lo1add  15469  lo1mul  15470  climcau  15515  climbdd  15516  caucvgb  15524  summo  15562  isumltss  15693  mertenslem2  15730  prodmolem2  15778  prodmo  15779  dvdsaddre2b  16149  bitsfzolem  16274  bitsfzo  16275  bezoutlem4  16383  lcmfeq0b  16466  lcmfunsnlem2  16476  divgcdcoprmex  16502  prmind2  16521  2mulprm  16529  isprm5  16543  prm23ge5  16647  pcqmul  16685  pcadd  16721  prmreclem2  16749  prmreclem5  16752  mul4sq  16786  vdwmc2  16811  ramcl  16861  prmgaplem7  16889  prmlem1a  16939  setsstruct2  17006  divsfval  17389  iscatd2  17521  catpropd  17549  wunfunc  17745  wunfuncOLD  17746  cyccom  18955  gaorber  19047  psgneu  19247  lsmsubm  19394  pj1eu  19437  efgredlem  19488  qusabl  19602  cygctb  19628  lt6abl  19631  gsumval3eu  19640  dprdsubg  19762  ablfac1c  19809  pgpfac1  19818  dvdsrtr  20034  unitgrp  20049  drngmul0or  20163  lvecvs0or  20522  lspdisjb  20540  lspsolvlem  20556  lspprat  20567  lbsextlem2  20573  abvn0b  20725  domnchr  20888  znfld  20920  cygznlem3  20929  obselocv  21087  cpmatacl  22017  chfacfisf  22155  chfacfisfcpmat  22156  0ntr  22374  opnneiid  22429  restntr  22485  hausnei2  22656  nrmsep3  22658  cmpsub  22703  uncmp  22706  dfconn2  22722  cnconn  22725  1stcfb  22748  txuni2  22868  txbas  22870  ptbasin  22880  txcls  22907  txbasval  22909  txlly  22939  txnlly  22940  pthaus  22941  txlm  22951  tx1stc  22953  xkohaus  22956  isufil2  23211  ufileu  23222  cnpflfi  23302  txflf  23309  fclscf  23328  flimfnfcls  23331  alexsubb  23349  alexsubALTlem2  23351  alexsubALTlem4  23353  ptcmplem2  23356  ptcmplem3  23357  cnextcn  23370  qustgplem  23424  prdsmet  23675  blin2  23734  prdsbl  23799  nmolb  24033  tgqioo  24115  reconnlem2  24142  reconn  24143  lebnumlem3  24278  iscau4  24595  cmetcaulem  24604  iscmet3lem2  24608  bcthlem5  24644  minveclem3b  24744  pmltpc  24766  evthicc2  24776  ovolunlem2  24814  ovolicc2lem5  24837  mblsplit  24848  iundisj2  24865  volsup  24872  ioombl1lem4  24877  dyaddisj  24912  dyadmbllem  24915  i1faddlem  25009  itg10a  25027  itg1ge0a  25028  mbfi1flimlem  25039  mbfmullem  25042  itg2add  25076  rolle  25306  dvcvx  25336  itgsubst  25365  tdeglem4  25376  tdeglem4OLD  25377  ply1domn  25440  fta1b  25486  plyadd  25530  plymul  25531  coeeu  25538  vieta1  25624  aalioulem6  25649  ulmcaulem  25705  ulmcau  25706  ulmbdd  25709  ulmcn  25710  amgm  26292  mumullem2  26481  ppiublem1  26502  dchrfi  26555  dchrptlem2  26565  dchrptlem3  26566  dchrsum2  26568  lgsdchr  26655  lgsquad2lem2  26685  2sqlem5  26722  2sqb  26732  pntlemp  26910  ostthlem2  26928  ostth  26939  nosupprefixmo  27000  noinfprefixmo  27001  noetasuplem4  27036  madebdaylemlrcut  27177  iscgrglt  27285  tgbtwnconn1  27346  colline  27420  lmimid  27565  axcontlem8  27749  axcontlem9  27750  eengtrkg  27764  numedglnl  27924  uhgr2edg  27985  uspgr2wlkeq  28423  wlkonl1iedg  28442  wlkdlem2  28460  pthdlem2  28545  clwlkclwwlklem2a4  28770  clwwisshclwwsn  28789  clwwlknon1sn  28873  frgr2wwlkeu  29100  frgrreg  29167  frgrregord013  29168  nvmul0or  29421  ubthlem3  29643  axhcompl-zf  29769  hvmul0or  29796  ocnel  30069  pjhthmo  30073  spanuni  30315  spansni  30328  hon0  30564  leopadd  30903  leoptr  30908  mdsymlem6  31179  sumdmdlem2  31190  cdjreui  31203  iundisj2f  31336  disjunsn  31340  iundisj2fi  31525  prmdvdsbc  31537  ballotlemimin  32909  bnj23  33134  bnj594  33328  bnj849  33341  cusgr3cyclex  33534  txsconn  33639  cvmsdisj  33668  cvmliftlem15  33696  cvmlift2lem10  33710  cvmlift3lem7  33723  fmla1  33785  satffunlem1lem2  33801  satffunlem2lem2  33804  mclsppslem  33981  dfon2lem3  34170  dfon2lem5  34172  dfon2lem6  34173  dfon2lem7  34174  dfon2lem8  34175  addsproplem2  34279  ifscgr  34561  cgr3tr4  34569  btwnconn1lem13  34616  seglecgr12  34628  elicc3  34721  neibastop1  34763  tailfb  34781  bj-sblem2  35241  bj-sngltag  35386  copsex2d  35542  mptsnunlem  35741  finxpreclem6  35799  wl-equsal1i  35934  lindsenlbs  36005  poimirlem26  36036  poimirlem27  36037  ismblfin  36051  itg2addnclem3  36063  ftc1anclem6  36088  fdc  36136  riscer  36379  intidl  36420  ispridlc  36461  disjlem14  37192  disjlem17  37193  prtlem14  37268  prtlem17  37270  lpssat  37407  lssatle  37409  lshpkrlem6  37509  cvrnbtwn  37665  atlatmstc  37713  atlatle  37714  atlrelat1  37715  2at0mat0  37920  trlator0  38566  cdleme0moN  38620  cdlemn11pre  39605  dihord2pre  39620  dihmeetlem20N  39721  dochkrshp4  39784  lcfl6  39895  remulid2  40805  diophin  40998  diophun  40999  inaex  42482  pm10.57  42556  fnchoice  43139  ellimcabssub0  43753  fourierdlem81  44323  fourierdlem93  44335  2reuimp0  45241  fzopredsuc  45450  2ffzoeq  45455  iccpartlt  45511  ichnreuop  45559  prmdvdsfmtnof1lem1  45671  lighneallem4  45697  odd2prm2  45805  even3prm2  45806  sbgoldbst  45865  nnsum4primesevenALTV  45888  nzerooringczr  46265  ply1mulgsumlem1  46362  snlindsntor  46447  islininds2  46460  m1modmmod  46502  itschlc0xyqsol1  46747  2itscp  46762  opnneir  46834  iscnrm3lem2  46862
  Copyright terms: Public domain W3C validator