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  294  oplem1  1055  nic-ax  1675  19.30  1884  19.33b  1888  necon1bd  2959  spc2d  3559  pssdifn0  4323  ralnralall  4474  disjss3  5102  somo  5579  frminex  5610  sofld  6135  predtrss  6272  ordelord  6335  unizlim  6435  f0rn0  6722  funopfv  6889  mpteqb  6962  fvrnressn  7101  funfvima  7174  fpropnf1  7208  fliftfun  7251  weniso  7293  tfinds  7786  tfindsg  7787  tfindes  7789  tfinds2  7790  findsg  7826  frxp  8046  soseq  8058  suppssr  8094  rdgsucmptnf  8342  frsucmptn  8352  tz7.49  8358  om00  8489  oewordi  8505  iiner  8661  eroveu  8684  fsetexb  8735  undomOLD  8937  sucdom2OLD  8959  sdomdif  9002  pssnn  9045  sucdom2  9083  php3  9089  php3OLD  9101  unxpdomlem3  9129  fisseneq  9134  pssnnOLD  9142  ordunifi  9170  isfinite2  9178  fiint  9201  infssuni  9220  ixpfi2  9227  finsschain  9236  ordtypelem10  9396  wofib  9414  wemapsolem  9419  unxpwdom2  9457  inf3lem2  9498  cantnfp1lem3  9549  cantnfp1  9550  setind  9603  frr3g  9625  r1tr  9645  r1ordg  9647  rankelb  9693  rankxplim3  9750  updjudhf  9800  cardlim  9841  infxpenlem  9882  infxpenc2  9891  dfac5lem4  9995  dfac12k  10016  kmlem13  10031  sornom  10146  fin23lem25  10193  fin23lem21  10208  zorn2lem4  10368  iundom2g  10409  fpwwe2lem11  10510  fpwwe2lem12  10511  pwfseqlem4a  10530  eltsk2g  10620  inttsk  10643  tskord  10649  r1tskina  10651  grudomon  10686  arch  12343  zaddcl  12473  uzm1  12729  xrsupsslem  13154  xrinfmsslem  13155  fsequb  13808  fseqsupubi  13811  ssnn0fi  13818  seqf1o  13877  sq01  14053  ccatalpha  14408  swrdnd0  14476  repsdf2  14597  cshw1  14641  wrdl3s3  14784  rexanre  15165  rexuzre  15171  cau3lem  15173  o1co  15402  rlimcn3  15406  o1of2  15429  lo1add  15443  lo1mul  15444  climcau  15489  climbdd  15490  caucvgb  15498  summo  15536  isumltss  15667  mertenslem2  15704  prodmolem2  15752  prodmo  15753  dvdsaddre2b  16123  bitsfzolem  16248  bitsfzo  16249  bezoutlem4  16357  lcmfeq0b  16440  lcmfunsnlem2  16450  divgcdcoprmex  16476  prmind2  16495  2mulprm  16503  isprm5  16517  prm23ge5  16621  pcqmul  16659  pcadd  16695  prmreclem2  16723  prmreclem5  16726  mul4sq  16760  vdwmc2  16785  ramcl  16835  prmgaplem7  16863  prmlem1a  16913  setsstruct2  16980  divsfval  17363  iscatd2  17495  catpropd  17523  wunfunc  17719  wunfuncOLD  17720  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  27254  tgbtwnconn1  27315  colline  27389  lmimid  27534  axcontlem8  27718  axcontlem9  27719  eengtrkg  27733  numedglnl  27893  uhgr2edg  27954  uspgr2wlkeq  28392  wlkonl1iedg  28411  wlkdlem2  28429  pthdlem2  28514  clwlkclwwlklem2a4  28739  clwwisshclwwsn  28758  clwwlknon1sn  28842  frgr2wwlkeu  29069  frgrreg  29136  frgrregord013  29137  nvmul0or  29390  ubthlem3  29612  axhcompl-zf  29738  hvmul0or  29765  ocnel  30038  pjhthmo  30042  spanuni  30284  spansni  30297  hon0  30533  leopadd  30872  leoptr  30877  mdsymlem6  31148  sumdmdlem2  31159  cdjreui  31172  iundisj2f  31305  disjunsn  31309  iundisj2fi  31494  prmdvdsbc  31506  ballotlemimin  32878  bnj23  33103  bnj594  33297  bnj849  33310  cusgr3cyclex  33503  txsconn  33608  cvmsdisj  33637  cvmliftlem15  33665  cvmlift2lem10  33679  cvmlift3lem7  33692  fmla1  33754  satffunlem1lem2  33770  satffunlem2lem2  33773  mclsppslem  33950  dfon2lem3  34150  dfon2lem5  34152  dfon2lem6  34153  dfon2lem7  34154  dfon2lem8  34155  poxp2  34178  poxp3  34184  addsproplem2  34272  ifscgr  34524  cgr3tr4  34532  btwnconn1lem13  34579  seglecgr12  34591  elicc3  34684  neibastop1  34726  tailfb  34744  bj-sblem2  35204  bj-sngltag  35349  copsex2d  35505  mptsnunlem  35704  finxpreclem6  35762  wl-equsal1i  35897  lindsenlbs  35968  poimirlem26  35999  poimirlem27  36000  ismblfin  36014  itg2addnclem3  36026  ftc1anclem6  36051  fdc  36099  riscer  36342  intidl  36383  ispridlc  36424  disjlem14  37155  disjlem17  37156  prtlem14  37231  prtlem17  37233  lpssat  37370  lssatle  37372  lshpkrlem6  37472  cvrnbtwn  37628  atlatmstc  37676  atlatle  37677  atlrelat1  37678  2at0mat0  37883  trlator0  38529  cdleme0moN  38583  cdlemn11pre  39568  dihord2pre  39583  dihmeetlem20N  39684  dochkrshp4  39747  lcfl6  39858  remulid2  40770  diophin  40960  diophun  40961  inaex  42341  pm10.57  42415  fnchoice  42998  ellimcabssub0  43611  fourierdlem81  44181  fourierdlem93  44193  2reuimp0  45095  fzopredsuc  45304  2ffzoeq  45309  iccpartlt  45365  ichnreuop  45413  prmdvdsfmtnof1lem1  45525  lighneallem4  45551  odd2prm2  45659  even3prm2  45660  sbgoldbst  45719  nnsum4primesevenALTV  45742  nzerooringczr  46119  ply1mulgsumlem1  46216  snlindsntor  46301  islininds2  46314  m1modmmod  46356  itschlc0xyqsol1  46601  2itscp  46616  opnneir  46688  iscnrm3lem2  46716
  Copyright terms: Public domain W3C validator