Theorem biimtrrid 243

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 228	. 2 ⊢ (𝜑 → 𝜓)
3		biimtrrid.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 34	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3imtr3g  295  oplem1  1056  nic-ax  1673  19.30  1881  19.33b  1885  necon1bd  2943  rexlimdvvva  3187  spc2d  3557  pssdifn0  4319  ralnralall  4466  disjss3  5091  somo  5566  frminex  5598  sofld  6136  predtrss  6270  ordelord  6329  unizlim  6431  f0rn0  6709  funopfv  6872  mpteqb  6949  fvrnressn  7095  funfvima  7166  fpropnf1  7204  fliftfun  7249  weniso  7291  tfinds  7793  tfindsg  7794  tfindes  7796  tfinds2  7797  findsg  7830  resf1ext2b  7868  frxp  8059  poxp2  8076  soseq  8092  suppssr  8128  rdgsucmptnf  8351  frsucmptn  8361  tz7.49  8367  om00  8493  oewordi  8509  iiner  8716  eroveu  8739  fsetexb  8791  sdomdif  9042  pssnn  9082  sucdom2  9117  php3  9123  unxpdomlem3  9147  fisseneq  9152  ordunifi  9179  isfinite2  9187  fiint  9216  fiintOLD  9217  infssuni  9236  ixpfi2  9240  finsschain  9249  ordtypelem10  9419  wofib  9437  wemapsolem  9442  unxpwdom2  9480  inf3lem2  9525  cantnfp1lem3  9576  cantnfp1  9577  setind  9630  frr3g  9652  r1tr  9672  r1ordg  9674  rankelb  9720  rankxplim3  9777  updjudhf  9827  cardlim  9868  infxpenlem  9907  infxpenc2  9916  dfac5lem4  10020  dfac5lem4OLD  10022  dfac12k  10042  kmlem13  10057  sornom  10171  fin23lem25  10218  fin23lem21  10233  zorn2lem4  10393  iundom2g  10434  fpwwe2lem11  10535  fpwwe2lem12  10536  pwfseqlem4a  10555  eltsk2g  10645  inttsk  10668  tskord  10674  r1tskina  10676  grudomon  10711  arch  12381  zaddcl  12515  uzm1  12773  xrsupsslem  13209  xrinfmsslem  13210  fsequb  13882  fseqsupubi  13885  ssnn0fi  13892  seqf1o  13950  sq01  14132  ccatalpha  14500  swrdnd0  14564  repsdf2  14684  cshw1  14728  wrdl3s3  14869  rexanre  15254  rexuzre  15260  cau3lem  15262  o1co  15493  rlimcn3  15497  o1of2  15520  lo1add  15534  lo1mul  15535  climcau  15578  climbdd  15579  caucvgb  15587  summo  15624  isumltss  15755  mertenslem2  15792  prodmolem2  15842  prodmo  15843  dvdsaddre2b  16218  bitsfzolem  16345  bitsfzo  16346  bezoutlem4  16453  lcmfeq0b  16541  lcmfunsnlem2  16551  divgcdcoprmex  16577  prmind2  16596  2mulprm  16604  isprm5  16618  prmdvdsbc  16637  prm23ge5  16727  pcqmul  16765  pcadd  16801  prmreclem2  16829  prmreclem5  16832  mul4sq  16866  vdwmc2  16891  ramcl  16941  prmgaplem7  16969  prmlem1a  17018  setsstruct2  17085  divsfval  17451  iscatd2  17587  catpropd  17615  wunfunc  17808  cyccom  19082  gaorber  19187  psgneu  19385  lsmsubm  19532  pj1eu  19575  efgredlem  19626  qusabl  19744  cygctb  19771  lt6abl  19774  gsumval3eu  19783  dprdsubg  19905  ablfac1c  19952  pgpfac1  19961  dvdsrtr  20253  unitgrp  20268  drngmul0orOLD  20646  abvn0b  20721  lvecvs0or  21015  lspdisjb  21033  lspsolvlem  21049  lspprat  21060  lbsextlem2  21066  nzerooringczr  21387  domnchr  21439  znfld  21467  cygznlem3  21476  obselocv  21635  cpmatacl  22601  chfacfisf  22739  chfacfisfcpmat  22740  0ntr  22956  opnneiid  23011  restntr  23067  hausnei2  23238  nrmsep3  23240  cmpsub  23285  uncmp  23288  dfconn2  23304  cnconn  23307  1stcfb  23330  txuni2  23450  txbas  23452  ptbasin  23462  txcls  23489  txbasval  23491  txlly  23521  txnlly  23522  pthaus  23523  txlm  23533  tx1stc  23535  xkohaus  23538  isufil2  23793  ufileu  23804  cnpflfi  23884  txflf  23891  fclscf  23910  flimfnfcls  23913  alexsubb  23931  alexsubALTlem2  23933  alexsubALTlem4  23935  ptcmplem2  23938  ptcmplem3  23939  cnextcn  23952  qustgplem  24006  prdsmet  24256  blin2  24315  prdsbl  24377  nmolb  24603  tgqioo  24686  reconnlem2  24714  reconn  24715  lebnumlem3  24860  iscau4  25177  cmetcaulem  25186  iscmet3lem2  25190  bcthlem5  25226  minveclem3b  25326  pmltpc  25349  evthicc2  25359  ovolunlem2  25397  ovolicc2lem5  25420  mblsplit  25431  iundisj2  25448  volsup  25455  ioombl1lem4  25460  dyaddisj  25495  dyadmbllem  25498  i1faddlem  25592  itg10a  25609  itg1ge0a  25610  mbfi1flimlem  25621  mbfmullem  25624  itg2add  25658  rolle  25892  dvcvx  25923  itgsubst  25954  tdeglem4  25963  ply1domn  26027  fta1b  26075  plyadd  26120  plymul  26121  coeeu  26128  vieta1  26218  aalioulem6  26243  ulmcaulem  26301  ulmcau  26302  ulmbdd  26305  ulmcn  26306  amgm  26899  mumullem2  27088  ppiublem1  27111  dchrfi  27164  dchrptlem2  27174  dchrptlem3  27175  dchrsum2  27177  lgsdchr  27264  lgsquad2lem2  27294  2sqlem5  27331  2sqb  27341  pntlemp  27519  ostthlem2  27537  ostth  27548  nosupprefixmo  27610  noinfprefixmo  27611  noetasuplem4  27646  madebdaylemlrcut  27813  addsproplem2  27882  precsexlem11  28124  sltonold  28167  iscgrglt  28459  tgbtwnconn1  28520  colline  28594  lmimid  28739  axcontlem8  28916  axcontlem9  28917  eengtrkg  28931  numedglnl  29089  uhgr2edg  29153  uspgr2wlkeq  29591  wlkonl1iedg  29609  wlkdlem2  29627  pthdlem2  29713  clwlkclwwlklem2a4  29941  clwwisshclwwsn  29960  clwwlknon1sn  30044  frgr2wwlkeu  30271  frgrreg  30338  frgrregord013  30339  nvmul0or  30594  ubthlem3  30816  axhcompl-zf  30942  hvmul0or  30969  ocnel  31242  pjhthmo  31246  spanuni  31488  spansni  31501  hon0  31737  leopadd  32076  leoptr  32081  mdsymlem6  32352  sumdmdlem2  32363  cdjreui  32376  iundisj2f  32534  disjunsn  32538  iundisj2fi  32740  ballotlemimin  34474  bnj23  34685  bnj594  34879  bnj849  34892  setindregs  35065  cusgr3cyclex  35109  txsconn  35214  cvmsdisj  35243  cvmliftlem15  35271  cvmlift2lem10  35285  cvmlift3lem7  35298  fmla1  35360  satffunlem1lem2  35376  satffunlem2lem2  35379  mclsppslem  35556  dfon2lem3  35759  dfon2lem5  35761  dfon2lem6  35762  dfon2lem7  35763  dfon2lem8  35764  ifscgr  36018  cgr3tr4  36026  btwnconn1lem13  36073  seglecgr12  36085  elicc3  36291  neibastop1  36333  tailfb  36351  bj-sblem2  36817  bj-sngltag  36957  copsex2d  37113  mptsnunlem  37312  finxpreclem6  37370  wl-equsal1i  37518  lindsenlbs  37595  poimirlem26  37626  poimirlem27  37627  ismblfin  37641  itg2addnclem3  37653  ftc1anclem6  37678  fdc  37725  riscer  37968  intidl  38009  ispridlc  38050  disjlem14  38776  disjlem17  38777  prtlem14  38853  prtlem17  38855  lpssat  38992  lssatle  38994  lshpkrlem6  39094  cvrnbtwn  39250  atlatmstc  39298  atlatle  39299  atlrelat1  39300  2at0mat0  39504  trlator0  40150  cdleme0moN  40204  cdlemn11pre  41189  dihord2pre  41204  dihmeetlem20N  41305  dochkrshp4  41368  lcfl6  41479  expeqidd  42298  remullid  42407  diophin  42745  diophun  42746  inaex  44270  pm10.57  44344  modelaxreplem1  44952  fnchoice  45007  ellimcabssub0  45598  fourierdlem81  46168  fourierdlem93  46180  2reuimp0  47098  fzopredsuc  47307  2ffzoeq  47311  m1modmmod  47342  iccpartlt  47408  ichnreuop  47456  prmdvdsfmtnof1lem1  47568  lighneallem4  47594  odd2prm2  47702  even3prm2  47703  sbgoldbst  47762  nnsum4primesevenALTV  47785  stgrvtx0  47946  isubgr3stgrlem6  47955  grlimprclnbgrvtx  47983  pgnbgreunbgr  48109  ply1mulgsumlem1  48371  snlindsntor  48456  islininds2  48469  itschlc0xyqsol1  48751  2itscp  48766  opnneir  48891  iscnrm3lem2  48919