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

Step	Hyp	Ref	Expression
1		biimtrrid.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	biimpri 227	. 2 ⊢ (𝜑 → 𝜓)
3		biimtrrid.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 34	1 ⊢ (𝜒 → (𝜑 → 𝜃))

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  1054  nic-ax  1668  19.30  1877  19.33b  1881  necon1bd  2948  spc2d  3587  pssdifn0  4361  ralnralall  4513  disjss3  5142  somo  5621  frminex  5652  sofld  6188  predtrss  6324  ordelord  6387  unizlim  6488  f0rn0  6776  funopfv  6942  mpteqb  7017  fvrnressn  7164  funfvima  7236  fpropnf1  7271  fliftfun  7313  weniso  7355  tfinds  7859  tfindsg  7860  tfindes  7862  tfinds2  7863  findsg  7899  frxp  8129  poxp2  8146  soseq  8162  suppssr  8199  rdgsucmptnf  8448  frsucmptn  8458  tz7.49  8464  om00  8594  oewordi  8610  iiner  8807  eroveu  8830  fsetexb  8882  undomOLD  9087  sucdom2OLD  9109  sdomdif  9152  pssnn  9195  sucdom2  9230  php3  9236  php3OLD  9248  unxpdomlem3  9276  fisseneq  9281  pssnnOLD  9289  ordunifi  9317  isfinite2  9325  fiint  9358  fiintOLD  9359  infssuni  9378  ixpfi2  9384  finsschain  9393  ordtypelem10  9560  wofib  9578  wemapsolem  9583  unxpwdom2  9621  inf3lem2  9662  cantnfp1lem3  9713  cantnfp1  9714  setind  9767  frr3g  9789  r1tr  9809  r1ordg  9811  rankelb  9857  rankxplim3  9914  updjudhf  9964  cardlim  10005  infxpenlem  10046  infxpenc2  10055  dfac5lem4  10159  dfac12k  10180  kmlem13  10195  sornom  10308  fin23lem25  10355  fin23lem21  10370  zorn2lem4  10530  iundom2g  10571  fpwwe2lem11  10672  fpwwe2lem12  10673  pwfseqlem4a  10692  eltsk2g  10782  inttsk  10805  tskord  10811  r1tskina  10813  grudomon  10848  arch  12512  zaddcl  12645  uzm1  12903  xrsupsslem  13331  xrinfmsslem  13332  fsequb  13986  fseqsupubi  13989  ssnn0fi  13996  seqf1o  14054  sq01  14234  ccatalpha  14593  swrdnd0  14657  repsdf2  14778  cshw1  14822  wrdl3s3  14963  rexanre  15343  rexuzre  15349  cau3lem  15351  o1co  15580  rlimcn3  15584  o1of2  15607  lo1add  15621  lo1mul  15622  climcau  15667  climbdd  15668  caucvgb  15676  summo  15713  isumltss  15844  mertenslem2  15881  prodmolem2  15929  prodmo  15930  dvdsaddre2b  16301  bitsfzolem  16426  bitsfzo  16427  bezoutlem4  16535  lcmfeq0b  16623  lcmfunsnlem2  16633  divgcdcoprmex  16659  prmind2  16678  2mulprm  16686  isprm5  16700  prmdvdsbc  16720  prm23ge5  16809  pcqmul  16847  pcadd  16883  prmreclem2  16911  prmreclem5  16914  mul4sq  16948  vdwmc2  16973  ramcl  17023  prmgaplem7  17051  prmlem1a  17101  setsstruct2  17168  divsfval  17554  iscatd2  17686  catpropd  17714  wunfunc  17912  wunfuncOLD  17913  cyccom  19190  gaorber  19295  psgneu  19497  lsmsubm  19644  pj1eu  19687  efgredlem  19738  qusabl  19856  cygctb  19883  lt6abl  19886  gsumval3eu  19895  dprdsubg  20017  ablfac1c  20064  pgpfac1  20073  dvdsrtr  20343  unitgrp  20358  drngmul0orOLD  20732  abvn0b  20808  lvecvs0or  21082  lspdisjb  21100  lspsolvlem  21116  lspprat  21127  lbsextlem2  21133  nzerooringczr  21463  domnchr  21519  znfld  21551  cygznlem3  21560  obselocv  21719  cpmatacl  22703  chfacfisf  22841  chfacfisfcpmat  22842  0ntr  23060  opnneiid  23115  restntr  23171  hausnei2  23342  nrmsep3  23344  cmpsub  23389  uncmp  23392  dfconn2  23408  cnconn  23411  1stcfb  23434  txuni2  23554  txbas  23556  ptbasin  23566  txcls  23593  txbasval  23595  txlly  23625  txnlly  23626  pthaus  23627  txlm  23637  tx1stc  23639  xkohaus  23642  isufil2  23897  ufileu  23908  cnpflfi  23988  txflf  23995  fclscf  24014  flimfnfcls  24017  alexsubb  24035  alexsubALTlem2  24037  alexsubALTlem4  24039  ptcmplem2  24042  ptcmplem3  24043  cnextcn  24056  qustgplem  24110  prdsmet  24361  blin2  24420  prdsbl  24485  nmolb  24719  tgqioo  24801  reconnlem2  24828  reconn  24829  lebnumlem3  24974  iscau4  25292  cmetcaulem  25301  iscmet3lem2  25305  bcthlem5  25341  minveclem3b  25441  pmltpc  25464  evthicc2  25474  ovolunlem2  25512  ovolicc2lem5  25535  mblsplit  25546  iundisj2  25563  volsup  25570  ioombl1lem4  25575  dyaddisj  25610  dyadmbllem  25613  i1faddlem  25707  itg10a  25725  itg1ge0a  25726  mbfi1flimlem  25737  mbfmullem  25740  itg2add  25774  rolle  26007  dvcvx  26038  itgsubst  26069  tdeglem4  26080  tdeglem4OLD  26081  ply1domn  26145  fta1b  26193  plyadd  26238  plymul  26239  coeeu  26246  vieta1  26334  aalioulem6  26359  ulmcaulem  26417  ulmcau  26418  ulmbdd  26421  ulmcn  26422  amgm  27013  mumullem2  27202  ppiublem1  27225  dchrfi  27278  dchrptlem2  27288  dchrptlem3  27289  dchrsum2  27291  lgsdchr  27378  lgsquad2lem2  27408  2sqlem5  27445  2sqb  27455  pntlemp  27633  ostthlem2  27651  ostth  27662  nosupprefixmo  27724  noinfprefixmo  27725  noetasuplem4  27760  madebdaylemlrcut  27916  addsproplem2  27978  precsexlem11  28210  sltonold  28248  iscgrglt  28435  tgbtwnconn1  28496  colline  28570  lmimid  28715  axcontlem8  28899  axcontlem9  28900  eengtrkg  28914  numedglnl  29074  uhgr2edg  29138  uspgr2wlkeq  29577  wlkonl1iedg  29596  wlkdlem2  29614  pthdlem2  29699  clwlkclwwlklem2a4  29924  clwwisshclwwsn  29943  clwwlknon1sn  30027  frgr2wwlkeu  30254  frgrreg  30321  frgrregord013  30322  nvmul0or  30577  ubthlem3  30799  axhcompl-zf  30925  hvmul0or  30952  ocnel  31225  pjhthmo  31229  spanuni  31471  spansni  31484  hon0  31720  leopadd  32059  leoptr  32064  mdsymlem6  32335  sumdmdlem2  32346  cdjreui  32359  iundisj2f  32507  disjunsn  32511  iundisj2fi  32699  ballotlemimin  34349  bnj23  34573  bnj594  34767  bnj849  34780  cusgr3cyclex  34974  txsconn  35079  cvmsdisj  35108  cvmliftlem15  35136  cvmlift2lem10  35150  cvmlift3lem7  35163  fmla1  35225  satffunlem1lem2  35241  satffunlem2lem2  35244  mclsppslem  35421  dfon2lem3  35619  dfon2lem5  35621  dfon2lem6  35622  dfon2lem7  35623  dfon2lem8  35624  ifscgr  35878  cgr3tr4  35886  btwnconn1lem13  35933  seglecgr12  35945  elicc3  36039  neibastop1  36081  tailfb  36099  bj-sblem2  36558  bj-sngltag  36700  copsex2d  36856  mptsnunlem  37055  finxpreclem6  37113  wl-equsal1i  37249  lindsenlbs  37326  poimirlem26  37357  poimirlem27  37358  ismblfin  37372  itg2addnclem3  37384  ftc1anclem6  37409  fdc  37456  riscer  37699  intidl  37740  ispridlc  37781  disjlem14  38506  disjlem17  38507  prtlem14  38582  prtlem17  38584  lpssat  38721  lssatle  38723  lshpkrlem6  38823  cvrnbtwn  38979  atlatmstc  39027  atlatle  39028  atlrelat1  39029  2at0mat0  39234  trlator0  39880  cdleme0moN  39934  cdlemn11pre  40919  dihord2pre  40934  dihmeetlem20N  41035  dochkrshp4  41098  lcfl6  41209  expeqidd  42048  remullid  42141  diophin  42463  diophun  42464  inaex  44005  pm10.57  44079  fnchoice  44662  ellimcabssub0  45271  fourierdlem81  45841  fourierdlem93  45853  2reuimp0  46760  fzopredsuc  46969  2ffzoeq  46973  iccpartlt  47029  ichnreuop  47077  prmdvdsfmtnof1lem1  47189  lighneallem4  47215  odd2prm2  47323  even3prm2  47324  sbgoldbst  47383  nnsum4primesevenALTV  47406  ply1mulgsumlem1  47802  snlindsntor  47887  islininds2  47900  m1modmmod  47942  itschlc0xyqsol1  48187  2itscp  48202  opnneir  48273  iscnrm3lem2  48301