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  1669  19.30  1878  19.33b  1882  necon1bd  2955  rexlimdvvva  3211  spc2d  3601  pssdifn0  4373  ralnralall  4520  disjss3  5146  somo  5634  frminex  5667  sofld  6208  predtrss  6344  ordelord  6407  unizlim  6508  f0rn0  6793  funopfv  6958  mpteqb  7034  fvrnressn  7180  funfvima  7249  fpropnf1  7286  fliftfun  7331  weniso  7373  tfinds  7880  tfindsg  7881  tfindes  7883  tfinds2  7884  findsg  7919  frxp  8149  poxp2  8166  soseq  8182  suppssr  8218  rdgsucmptnf  8467  frsucmptn  8477  tz7.49  8483  om00  8611  oewordi  8627  iiner  8827  eroveu  8850  fsetexb  8902  undomOLD  9098  sucdom2OLD  9120  sdomdif  9163  pssnn  9206  sucdom2  9240  php3  9246  php3OLD  9258  unxpdomlem3  9285  fisseneq  9290  ordunifi  9323  isfinite2  9331  fiint  9363  fiintOLD  9364  infssuni  9383  ixpfi2  9387  finsschain  9396  ordtypelem10  9564  wofib  9582  wemapsolem  9587  unxpwdom2  9625  inf3lem2  9666  cantnfp1lem3  9717  cantnfp1  9718  setind  9771  frr3g  9793  r1tr  9813  r1ordg  9815  rankelb  9861  rankxplim3  9918  updjudhf  9968  cardlim  10009  infxpenlem  10050  infxpenc2  10059  dfac5lem4  10163  dfac5lem4OLD  10165  dfac12k  10185  kmlem13  10200  sornom  10314  fin23lem25  10361  fin23lem21  10376  zorn2lem4  10536  iundom2g  10577  fpwwe2lem11  10678  fpwwe2lem12  10679  pwfseqlem4a  10698  eltsk2g  10788  inttsk  10811  tskord  10817  r1tskina  10819  grudomon  10854  arch  12520  zaddcl  12654  uzm1  12913  xrsupsslem  13345  xrinfmsslem  13346  fsequb  14012  fseqsupubi  14015  ssnn0fi  14022  seqf1o  14080  sq01  14260  ccatalpha  14627  swrdnd0  14691  repsdf2  14812  cshw1  14856  wrdl3s3  14997  rexanre  15381  rexuzre  15387  cau3lem  15389  o1co  15618  rlimcn3  15622  o1of2  15645  lo1add  15659  lo1mul  15660  climcau  15703  climbdd  15704  caucvgb  15712  summo  15749  isumltss  15880  mertenslem2  15917  prodmolem2  15967  prodmo  15968  dvdsaddre2b  16340  bitsfzolem  16467  bitsfzo  16468  bezoutlem4  16575  lcmfeq0b  16663  lcmfunsnlem2  16673  divgcdcoprmex  16699  prmind2  16718  2mulprm  16726  isprm5  16740  prmdvdsbc  16759  prm23ge5  16848  pcqmul  16886  pcadd  16922  prmreclem2  16950  prmreclem5  16953  mul4sq  16987  vdwmc2  17012  ramcl  17062  prmgaplem7  17090  prmlem1a  17140  setsstruct2  17207  divsfval  17593  iscatd2  17725  catpropd  17753  wunfunc  17951  wunfuncOLD  17952  cyccom  19233  gaorber  19338  psgneu  19538  lsmsubm  19685  pj1eu  19728  efgredlem  19779  qusabl  19897  cygctb  19924  lt6abl  19927  gsumval3eu  19936  dprdsubg  20058  ablfac1c  20105  pgpfac1  20114  dvdsrtr  20384  unitgrp  20399  drngmul0orOLD  20777  abvn0b  20853  lvecvs0or  21127  lspdisjb  21145  lspsolvlem  21161  lspprat  21172  lbsextlem2  21178  nzerooringczr  21508  domnchr  21564  znfld  21596  cygznlem3  21605  obselocv  21765  cpmatacl  22737  chfacfisf  22875  chfacfisfcpmat  22876  0ntr  23094  opnneiid  23149  restntr  23205  hausnei2  23376  nrmsep3  23378  cmpsub  23423  uncmp  23426  dfconn2  23442  cnconn  23445  1stcfb  23468  txuni2  23588  txbas  23590  ptbasin  23600  txcls  23627  txbasval  23629  txlly  23659  txnlly  23660  pthaus  23661  txlm  23671  tx1stc  23673  xkohaus  23676  isufil2  23931  ufileu  23942  cnpflfi  24022  txflf  24029  fclscf  24048  flimfnfcls  24051  alexsubb  24069  alexsubALTlem2  24071  alexsubALTlem4  24073  ptcmplem2  24076  ptcmplem3  24077  cnextcn  24090  qustgplem  24144  prdsmet  24395  blin2  24454  prdsbl  24519  nmolb  24753  tgqioo  24835  reconnlem2  24862  reconn  24863  lebnumlem3  25008  iscau4  25326  cmetcaulem  25335  iscmet3lem2  25339  bcthlem5  25375  minveclem3b  25475  pmltpc  25498  evthicc2  25508  ovolunlem2  25546  ovolicc2lem5  25569  mblsplit  25580  iundisj2  25597  volsup  25604  ioombl1lem4  25609  dyaddisj  25644  dyadmbllem  25647  i1faddlem  25741  itg10a  25759  itg1ge0a  25760  mbfi1flimlem  25771  mbfmullem  25774  itg2add  25808  rolle  26042  dvcvx  26073  itgsubst  26104  tdeglem4  26113  ply1domn  26177  fta1b  26225  plyadd  26270  plymul  26271  coeeu  26278  vieta1  26368  aalioulem6  26393  ulmcaulem  26451  ulmcau  26452  ulmbdd  26455  ulmcn  26456  amgm  27048  mumullem2  27237  ppiublem1  27260  dchrfi  27313  dchrptlem2  27323  dchrptlem3  27324  dchrsum2  27326  lgsdchr  27413  lgsquad2lem2  27443  2sqlem5  27480  2sqb  27490  pntlemp  27668  ostthlem2  27686  ostth  27697  nosupprefixmo  27759  noinfprefixmo  27760  noetasuplem4  27795  madebdaylemlrcut  27951  addsproplem2  28017  precsexlem11  28255  sltonold  28297  iscgrglt  28536  tgbtwnconn1  28597  colline  28671  lmimid  28816  axcontlem8  29000  axcontlem9  29001  eengtrkg  29015  numedglnl  29175  uhgr2edg  29239  uspgr2wlkeq  29678  wlkonl1iedg  29697  wlkdlem2  29715  pthdlem2  29800  clwlkclwwlklem2a4  30025  clwwisshclwwsn  30044  clwwlknon1sn  30128  frgr2wwlkeu  30355  frgrreg  30422  frgrregord013  30423  nvmul0or  30678  ubthlem3  30900  axhcompl-zf  31026  hvmul0or  31053  ocnel  31326  pjhthmo  31330  spanuni  31572  spansni  31585  hon0  31821  leopadd  32160  leoptr  32165  mdsymlem6  32436  sumdmdlem2  32447  cdjreui  32460  iundisj2f  32609  disjunsn  32613  iundisj2fi  32804  ballotlemimin  34486  bnj23  34710  bnj594  34904  bnj849  34917  cusgr3cyclex  35120  txsconn  35225  cvmsdisj  35254  cvmliftlem15  35282  cvmlift2lem10  35296  cvmlift3lem7  35309  fmla1  35371  satffunlem1lem2  35387  satffunlem2lem2  35390  mclsppslem  35567  dfon2lem3  35766  dfon2lem5  35768  dfon2lem6  35769  dfon2lem7  35770  dfon2lem8  35771  ifscgr  36025  cgr3tr4  36033  btwnconn1lem13  36080  seglecgr12  36092  elicc3  36299  neibastop1  36341  tailfb  36359  bj-sblem2  36825  bj-sngltag  36965  copsex2d  37121  mptsnunlem  37320  finxpreclem6  37378  wl-equsal1i  37524  lindsenlbs  37601  poimirlem26  37632  poimirlem27  37633  ismblfin  37647  itg2addnclem3  37659  ftc1anclem6  37684  fdc  37731  riscer  37974  intidl  38015  ispridlc  38056  disjlem14  38779  disjlem17  38780  prtlem14  38855  prtlem17  38857  lpssat  38994  lssatle  38996  lshpkrlem6  39096  cvrnbtwn  39252  atlatmstc  39300  atlatle  39301  atlrelat1  39302  2at0mat0  39507  trlator0  40153  cdleme0moN  40207  cdlemn11pre  41192  dihord2pre  41207  dihmeetlem20N  41308  dochkrshp4  41371  lcfl6  41482  expeqidd  42338  remullid  42439  diophin  42759  diophun  42760  inaex  44292  pm10.57  44366  modelaxreplem1  44942  fnchoice  44966  ellimcabssub0  45572  fourierdlem81  46142  fourierdlem93  46154  2reuimp0  47063  fzopredsuc  47272  2ffzoeq  47276  iccpartlt  47348  ichnreuop  47396  prmdvdsfmtnof1lem1  47508  lighneallem4  47534  odd2prm2  47642  even3prm2  47643  sbgoldbst  47702  nnsum4primesevenALTV  47725  stgrvtx0  47864  isubgr3stgrlem6  47873  ply1mulgsumlem1  48231  snlindsntor  48316  islininds2  48329  m1modmmod  48370  itschlc0xyqsol1  48615  2itscp  48630  opnneir  48702  iscnrm3lem2  48730