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  1057  nic-ax  1675  19.30  1883  19.33b  1887  necon1bd  2950  rexlimdvvva  3195  spc2d  3544  pssdifn0  4308  ralnralall  4453  disjss3  5084  somo  5578  frminex  5610  sofld  6151  predtrss  6286  ordelord  6345  unizlim  6447  f0rn0  6725  funopfv  6889  mpteqb  6967  fvrnressn  7115  funfvima  7185  fpropnf1  7222  fliftfun  7267  weniso  7309  tfinds  7811  tfindsg  7812  tfindes  7814  tfinds2  7815  findsg  7848  resf1ext2b  7886  frxp  8076  poxp2  8093  soseq  8109  suppssr  8145  rdgsucmptnf  8368  frsucmptn  8378  tz7.49  8384  om00  8510  oewordi  8527  iiner  8736  eroveu  8759  fsetexb  8811  sdomdif  9063  pssnn  9103  sucdom2  9137  php3  9143  unxpdomlem3  9168  fisseneq  9173  ordunifi  9200  isfinite2  9208  fiint  9237  infssuni  9256  ixpfi2  9260  finsschain  9269  ordtypelem10  9442  wofib  9460  wemapsolem  9465  unxpwdom2  9503  inf3lem2  9550  cantnfp1lem3  9601  cantnfp1  9602  setind  9668  frr3g  9680  r1tr  9700  r1ordg  9702  rankelb  9748  rankxplim3  9805  updjudhf  9855  cardlim  9896  infxpenlem  9935  infxpenc2  9944  dfac5lem4  10048  dfac5lem4OLD  10050  dfac12k  10070  kmlem13  10085  sornom  10199  fin23lem25  10246  fin23lem21  10261  zorn2lem4  10421  iundom2g  10462  fpwwe2lem11  10564  fpwwe2lem12  10565  pwfseqlem4a  10584  eltsk2g  10674  inttsk  10697  tskord  10703  r1tskina  10705  grudomon  10740  arch  12434  zaddcl  12567  uzm1  12822  xrsupsslem  13259  xrinfmsslem  13260  fsequb  13937  fseqsupubi  13940  ssnn0fi  13947  seqf1o  14005  sq01  14187  ccatalpha  14556  swrdnd0  14620  repsdf2  14740  cshw1  14784  wrdl3s3  14924  rexanre  15309  rexuzre  15315  cau3lem  15317  o1co  15548  rlimcn3  15552  o1of2  15575  lo1add  15589  lo1mul  15590  climcau  15633  climbdd  15634  caucvgb  15642  summo  15679  isumltss  15813  mertenslem2  15850  prodmolem2  15900  prodmo  15901  dvdsaddre2b  16276  bitsfzolem  16403  bitsfzo  16404  bezoutlem4  16511  lcmfeq0b  16599  lcmfunsnlem2  16609  divgcdcoprmex  16635  prmind2  16654  2mulprm  16662  isprm5  16677  prmdvdsbc  16696  prm23ge5  16786  pcqmul  16824  pcadd  16860  prmreclem2  16888  prmreclem5  16891  mul4sq  16925  vdwmc2  16950  ramcl  17000  prmgaplem7  17028  prmlem1a  17077  setsstruct2  17144  divsfval  17511  iscatd2  17647  catpropd  17675  wunfunc  17868  cyccom  19178  gaorber  19283  psgneu  19481  lsmsubm  19628  pj1eu  19671  efgredlem  19722  qusabl  19840  cygctb  19867  lt6abl  19870  gsumval3eu  19879  dprdsubg  20001  ablfac1c  20048  pgpfac1  20057  dvdsrtr  20348  unitgrp  20363  drngmul0orOLD  20738  abvn0b  20813  lvecvs0or  21106  lspdisjb  21124  lspsolvlem  21140  lspprat  21151  lbsextlem2  21157  nzerooringczr  21460  domnchr  21512  znfld  21540  cygznlem3  21549  obselocv  21708  cpmatacl  22681  chfacfisf  22819  chfacfisfcpmat  22820  0ntr  23036  opnneiid  23091  restntr  23147  hausnei2  23318  nrmsep3  23320  cmpsub  23365  uncmp  23368  dfconn2  23384  cnconn  23387  1stcfb  23410  txuni2  23530  txbas  23532  ptbasin  23542  txcls  23569  txbasval  23571  txlly  23601  txnlly  23602  pthaus  23603  txlm  23613  tx1stc  23615  xkohaus  23618  isufil2  23873  ufileu  23884  cnpflfi  23964  txflf  23971  fclscf  23990  flimfnfcls  23993  alexsubb  24011  alexsubALTlem2  24013  alexsubALTlem4  24015  ptcmplem2  24018  ptcmplem3  24019  cnextcn  24032  qustgplem  24086  prdsmet  24335  blin2  24394  prdsbl  24456  nmolb  24682  tgqioo  24765  reconnlem2  24793  reconn  24794  lebnumlem3  24930  iscau4  25246  cmetcaulem  25255  iscmet3lem2  25259  bcthlem5  25295  minveclem3b  25395  pmltpc  25417  evthicc2  25427  ovolunlem2  25465  ovolicc2lem5  25488  mblsplit  25499  iundisj2  25516  volsup  25523  ioombl1lem4  25528  dyaddisj  25563  dyadmbllem  25566  i1faddlem  25660  itg10a  25677  itg1ge0a  25678  mbfi1flimlem  25689  mbfmullem  25692  itg2add  25726  rolle  25957  dvcvx  25987  itgsubst  26016  tdeglem4  26025  ply1domn  26089  fta1b  26137  plyadd  26182  plymul  26183  coeeu  26190  vieta1  26278  aalioulem6  26303  ulmcaulem  26359  ulmcau  26360  ulmbdd  26363  ulmcn  26364  amgm  26954  mumullem2  27143  ppiublem1  27165  dchrfi  27218  dchrptlem2  27228  dchrptlem3  27229  dchrsum2  27231  lgsdchr  27318  lgsquad2lem2  27348  2sqlem5  27385  2sqb  27395  pntlemp  27573  ostthlem2  27591  ostth  27602  nosupprefixmo  27664  noinfprefixmo  27665  noetasuplem4  27700  madebdaylemlrcut  27891  addsproplem2  27962  precsexlem11  28209  ltonold  28253  bdayfinbndlem1  28459  iscgrglt  28582  tgbtwnconn1  28643  colline  28717  lmimid  28862  axcontlem8  29040  axcontlem9  29041  eengtrkg  29055  numedglnl  29213  uhgr2edg  29277  uspgr2wlkeq  29714  wlkonl1iedg  29732  wlkdlem2  29750  pthdlem2  29836  clwlkclwwlklem2a4  30067  clwwisshclwwsn  30086  clwwlknon1sn  30170  frgr2wwlkeu  30397  frgrreg  30464  frgrregord013  30465  nvmul0or  30721  ubthlem3  30943  axhcompl-zf  31069  hvmul0or  31096  ocnel  31369  pjhthmo  31373  spanuni  31615  spansni  31628  hon0  31864  leopadd  32203  leoptr  32208  mdsymlem6  32479  sumdmdlem2  32490  cdjreui  32503  iundisj2f  32660  disjunsn  32664  iundisj2fi  32870  ballotlemimin  34650  bnj23  34861  bnj594  35054  bnj849  35067  setindregs  35274  cusgr3cyclex  35318  txsconn  35423  cvmsdisj  35452  cvmliftlem15  35480  cvmlift2lem10  35494  cvmlift3lem7  35507  fmla1  35569  satffunlem1lem2  35585  satffunlem2lem2  35588  mclsppslem  35765  dfon2lem3  35965  dfon2lem5  35967  dfon2lem6  35968  dfon2lem7  35969  dfon2lem8  35970  ifscgr  36226  cgr3tr4  36234  btwnconn1lem13  36281  seglecgr12  36293  elicc3  36499  neibastop1  36541  tailfb  36559  bj-sblem2  37150  bj-sngltag  37290  copsex2d  37453  mptsnunlem  37654  finxpreclem6  37712  wl-equsal1i  37869  lindsenlbs  37936  poimirlem26  37967  poimirlem27  37968  ismblfin  37982  itg2addnclem3  37994  ftc1anclem6  38019  fdc  38066  riscer  38309  intidl  38350  ispridlc  38391  disjlem14  39222  disjlem17  39223  prtlem14  39320  prtlem17  39322  lpssat  39459  lssatle  39461  lshpkrlem6  39561  cvrnbtwn  39717  atlatmstc  39765  atlatle  39766  atlrelat1  39767  2at0mat0  39971  trlator0  40617  cdleme0moN  40671  cdlemn11pre  41656  dihord2pre  41671  dihmeetlem20N  41772  dochkrshp4  41835  lcfl6  41946  expeqidd  42757  remullid  42866  diophin  43204  diophun  43205  inaex  44724  pm10.57  44798  modelaxreplem1  45405  fnchoice  45460  ellimcabssub0  46047  fourierdlem81  46615  fourierdlem93  46627  2reuimp0  47562  fzopredsuc  47772  2ffzoeq  47776  m1modmmod  47812  iccpartlt  47884  ichnreuop  47932  prmdvdsfmtnof1lem1  48047  lighneallem4  48073  odd2prm2  48194  even3prm2  48195  sbgoldbst  48254  nnsum4primesevenALTV  48277  stgrvtx0  48438  isubgr3stgrlem6  48447  grlimprclnbgrvtx  48475  pgnbgreunbgr  48601  ply1mulgsumlem1  48862  snlindsntor  48947  islininds2  48960  itschlc0xyqsol1  49242  2itscp  49257  opnneir  49382  iscnrm3lem2  49410