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  5580  frminex  5611  sofld  6136  predtrss  6273  ordelord  6336  unizlim  6436  f0rn0  6723  funopfv  6890  mpteqb  6963  fvrnressn  7102  funfvima  7175  fpropnf1  7209  fliftfun  7252  weniso  7294  tfinds  7787  tfindsg  7788  tfindes  7790  tfinds2  7791  findsg  7827  frxp  8047  soseq  8059  suppssr  8095  rdgsucmptnf  8343  frsucmptn  8353  tz7.49  8359  om00  8490  oewordi  8506  iiner  8662  eroveu  8685  fsetexb  8736  undomOLD  8938  sucdom2OLD  8960  sdomdif  9003  pssnn  9046  sucdom2  9084  php3  9090  php3OLD  9102  unxpdomlem3  9130  fisseneq  9135  pssnnOLD  9143  ordunifi  9171  isfinite2  9179  fiint  9202  infssuni  9221  ixpfi2  9228  finsschain  9237  ordtypelem10  9397  wofib  9415  wemapsolem  9420  unxpwdom2  9458  inf3lem2  9499  cantnfp1lem3  9550  cantnfp1  9551  setind  9604  frr3g  9626  r1tr  9646  r1ordg  9648  rankelb  9694  rankxplim3  9751  updjudhf  9801  cardlim  9842  infxpenlem  9883  infxpenc2  9892  dfac5lem4  9996  dfac12k  10017  kmlem13  10032  sornom  10147  fin23lem25  10194  fin23lem21  10209  zorn2lem4  10369  iundom2g  10410  fpwwe2lem11  10511  fpwwe2lem12  10512  pwfseqlem4a  10531  eltsk2g  10621  inttsk  10644  tskord  10650  r1tskina  10652  grudomon  10687  arch  12344  zaddcl  12474  uzm1  12730  xrsupsslem  13155  xrinfmsslem  13156  fsequb  13809  fseqsupubi  13812  ssnn0fi  13819  seqf1o  13878  sq01  14054  ccatalpha  14409  swrdnd0  14477  repsdf2  14598  cshw1  14642  wrdl3s3  14785  rexanre  15166  rexuzre  15172  cau3lem  15174  o1co  15403  rlimcn3  15407  o1of2  15430  lo1add  15444  lo1mul  15445  climcau  15490  climbdd  15491  caucvgb  15499  summo  15537  isumltss  15668  mertenslem2  15705  prodmolem2  15753  prodmo  15754  dvdsaddre2b  16124  bitsfzolem  16249  bitsfzo  16250  bezoutlem4  16358  lcmfeq0b  16441  lcmfunsnlem2  16451  divgcdcoprmex  16477  prmind2  16496  2mulprm  16504  isprm5  16518  prm23ge5  16622  pcqmul  16660  pcadd  16696  prmreclem2  16724  prmreclem5  16727  mul4sq  16761  vdwmc2  16786  ramcl  16836  prmgaplem7  16864  prmlem1a  16914  setsstruct2  16981  divsfval  17364  iscatd2  17496  catpropd  17524  wunfunc  17720  wunfuncOLD  17721  cyccom  18928  gaorber  19020  psgneu  19220  lsmsubm  19364  pj1eu  19407  efgredlem  19458  qusabl  19572  cygctb  19598  lt6abl  19601  gsumval3eu  19610  dprdsubg  19732  ablfac1c  19779  pgpfac1  19788  dvdsrtr  20004  unitgrp  20019  drngmul0or  20133  lvecvs0or  20492  lspdisjb  20510  lspsolvlem  20526  lspprat  20537  lbsextlem2  20543  abvn0b  20695  domnchr  20858  znfld  20890  cygznlem3  20899  obselocv  21057  cpmatacl  21987  chfacfisf  22125  chfacfisfcpmat  22126  0ntr  22344  opnneiid  22399  restntr  22455  hausnei2  22626  nrmsep3  22628  cmpsub  22673  uncmp  22676  dfconn2  22692  cnconn  22695  1stcfb  22718  txuni2  22838  txbas  22840  ptbasin  22850  txcls  22877  txbasval  22879  txlly  22909  txnlly  22910  pthaus  22911  txlm  22921  tx1stc  22923  xkohaus  22926  isufil2  23181  ufileu  23192  cnpflfi  23272  txflf  23279  fclscf  23298  flimfnfcls  23301  alexsubb  23319  alexsubALTlem2  23321  alexsubALTlem4  23323  ptcmplem2  23326  ptcmplem3  23327  cnextcn  23340  qustgplem  23394  prdsmet  23645  blin2  23704  prdsbl  23769  nmolb  24003  tgqioo  24085  reconnlem2  24112  reconn  24113  lebnumlem3  24248  iscau4  24565  cmetcaulem  24574  iscmet3lem2  24578  bcthlem5  24614  minveclem3b  24714  pmltpc  24736  evthicc2  24746  ovolunlem2  24784  ovolicc2lem5  24807  mblsplit  24818  iundisj2  24835  volsup  24842  ioombl1lem4  24847  dyaddisj  24882  dyadmbllem  24885  i1faddlem  24979  itg10a  24997  itg1ge0a  24998  mbfi1flimlem  25009  mbfmullem  25012  itg2add  25046  rolle  25276  dvcvx  25306  itgsubst  25335  tdeglem4  25346  tdeglem4OLD  25347  ply1domn  25410  fta1b  25456  plyadd  25500  plymul  25501  coeeu  25508  vieta1  25594  aalioulem6  25619  ulmcaulem  25675  ulmcau  25676  ulmbdd  25679  ulmcn  25680  amgm  26262  mumullem2  26451  ppiublem1  26472  dchrfi  26525  dchrptlem2  26535  dchrptlem3  26536  dchrsum2  26538  lgsdchr  26625  lgsquad2lem2  26655  2sqlem5  26692  2sqb  26702  pntlemp  26880  ostthlem2  26898  ostth  26909  nosupprefixmo  26970  noinfprefixmo  26971  noetasuplem4  27006  madebdaylemlrcut  27146  iscgrglt  27242  tgbtwnconn1  27303  colline  27377  lmimid  27522  axcontlem8  27706  axcontlem9  27707  eengtrkg  27721  numedglnl  27881  uhgr2edg  27942  uspgr2wlkeq  28380  wlkonl1iedg  28399  wlkdlem2  28417  pthdlem2  28502  clwlkclwwlklem2a4  28727  clwwisshclwwsn  28746  clwwlknon1sn  28830  frgr2wwlkeu  29057  frgrreg  29124  frgrregord013  29125  nvmul0or  29378  ubthlem3  29600  axhcompl-zf  29726  hvmul0or  29753  ocnel  30026  pjhthmo  30030  spanuni  30272  spansni  30285  hon0  30521  leopadd  30860  leoptr  30865  mdsymlem6  31136  sumdmdlem2  31147  cdjreui  31160  iundisj2f  31293  disjunsn  31297  iundisj2fi  31482  prmdvdsbc  31494  ballotlemimin  32866  bnj23  33091  bnj594  33285  bnj849  33298  cusgr3cyclex  33491  txsconn  33596  cvmsdisj  33625  cvmliftlem15  33653  cvmlift2lem10  33667  cvmlift3lem7  33680  fmla1  33742  satffunlem1lem2  33758  satffunlem2lem2  33761  mclsppslem  33938  dfon2lem3  34138  dfon2lem5  34140  dfon2lem6  34141  dfon2lem7  34142  dfon2lem8  34143  poxp2  34166  poxp3  34172  addsproplem2  34266  ifscgr  34515  cgr3tr4  34523  btwnconn1lem13  34570  seglecgr12  34582  elicc3  34675  neibastop1  34717  tailfb  34735  bj-sblem2  35195  bj-sngltag  35340  copsex2d  35496  mptsnunlem  35695  finxpreclem6  35753  wl-equsal1i  35888  lindsenlbs  35959  poimirlem26  35990  poimirlem27  35991  ismblfin  36005  itg2addnclem3  36017  ftc1anclem6  36042  fdc  36090  riscer  36333  intidl  36374  ispridlc  36415  disjlem14  37146  disjlem17  37147  prtlem14  37222  prtlem17  37224  lpssat  37361  lssatle  37363  lshpkrlem6  37463  cvrnbtwn  37619  atlatmstc  37667  atlatle  37668  atlrelat1  37669  2at0mat0  37874  trlator0  38520  cdleme0moN  38574  cdlemn11pre  39559  dihord2pre  39574  dihmeetlem20N  39675  dochkrshp4  39738  lcfl6  39849  remulid2  40748  diophin  40929  diophun  40930  inaex  42310  pm10.57  42384  fnchoice  42967  ellimcabssub0  43568  fourierdlem81  44138  fourierdlem93  44150  2reuimp0  45046  fzopredsuc  45255
  Copyright terms: Public domain W3C validator