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  3554  pssdifn0  4315  ralnralall  4462  disjss3  5087  somo  5560  frminex  5592  sofld  6130  predtrss  6264  ordelord  6323  unizlim  6425  f0rn0  6703  funopfv  6865  mpteqb  6942  fvrnressn  7088  funfvima  7158  fpropnf1  7195  fliftfun  7240  weniso  7282  tfinds  7784  tfindsg  7785  tfindes  7787  tfinds2  7788  findsg  7821  resf1ext2b  7859  frxp  8050  poxp2  8067  soseq  8083  suppssr  8119  rdgsucmptnf  8342  frsucmptn  8352  tz7.49  8358  om00  8484  oewordi  8500  iiner  8707  eroveu  8730  fsetexb  8782  sdomdif  9032  pssnn  9072  sucdom2  9106  php3  9112  unxpdomlem3  9136  fisseneq  9141  ordunifi  9168  isfinite2  9176  fiint  9205  infssuni  9224  ixpfi2  9228  finsschain  9237  ordtypelem10  9407  wofib  9425  wemapsolem  9430  unxpwdom2  9468  inf3lem2  9513  cantnfp1lem3  9564  cantnfp1  9565  setind  9618  frr3g  9640  r1tr  9660  r1ordg  9662  rankelb  9708  rankxplim3  9765  updjudhf  9815  cardlim  9856  infxpenlem  9895  infxpenc2  9904  dfac5lem4  10008  dfac5lem4OLD  10010  dfac12k  10030  kmlem13  10045  sornom  10159  fin23lem25  10206  fin23lem21  10221  zorn2lem4  10381  iundom2g  10422  fpwwe2lem11  10523  fpwwe2lem12  10524  pwfseqlem4a  10543  eltsk2g  10633  inttsk  10656  tskord  10662  r1tskina  10664  grudomon  10699  arch  12369  zaddcl  12503  uzm1  12761  xrsupsslem  13197  xrinfmsslem  13198  fsequb  13870  fseqsupubi  13873  ssnn0fi  13880  seqf1o  13938  sq01  14120  ccatalpha  14488  swrdnd0  14552  repsdf2  14672  cshw1  14716  wrdl3s3  14856  rexanre  15241  rexuzre  15247  cau3lem  15249  o1co  15480  rlimcn3  15484  o1of2  15507  lo1add  15521  lo1mul  15522  climcau  15565  climbdd  15566  caucvgb  15574  summo  15611  isumltss  15742  mertenslem2  15779  prodmolem2  15829  prodmo  15830  dvdsaddre2b  16205  bitsfzolem  16332  bitsfzo  16333  bezoutlem4  16440  lcmfeq0b  16528  lcmfunsnlem2  16538  divgcdcoprmex  16564  prmind2  16583  2mulprm  16591  isprm5  16605  prmdvdsbc  16624  prm23ge5  16714  pcqmul  16752  pcadd  16788  prmreclem2  16816  prmreclem5  16819  mul4sq  16853  vdwmc2  16878  ramcl  16928  prmgaplem7  16956  prmlem1a  17005  setsstruct2  17072  divsfval  17438  iscatd2  17574  catpropd  17602  wunfunc  17795  cyccom  19069  gaorber  19174  psgneu  19372  lsmsubm  19519  pj1eu  19562  efgredlem  19613  qusabl  19731  cygctb  19758  lt6abl  19761  gsumval3eu  19770  dprdsubg  19892  ablfac1c  19939  pgpfac1  19948  dvdsrtr  20240  unitgrp  20255  drngmul0orOLD  20630  abvn0b  20705  lvecvs0or  20999  lspdisjb  21017  lspsolvlem  21033  lspprat  21044  lbsextlem2  21050  nzerooringczr  21371  domnchr  21423  znfld  21451  cygznlem3  21460  obselocv  21619  cpmatacl  22585  chfacfisf  22723  chfacfisfcpmat  22724  0ntr  22940  opnneiid  22995  restntr  23051  hausnei2  23222  nrmsep3  23224  cmpsub  23269  uncmp  23272  dfconn2  23288  cnconn  23291  1stcfb  23314  txuni2  23434  txbas  23436  ptbasin  23446  txcls  23473  txbasval  23475  txlly  23505  txnlly  23506  pthaus  23507  txlm  23517  tx1stc  23519  xkohaus  23522  isufil2  23777  ufileu  23788  cnpflfi  23868  txflf  23875  fclscf  23894  flimfnfcls  23897  alexsubb  23915  alexsubALTlem2  23917  alexsubALTlem4  23919  ptcmplem2  23922  ptcmplem3  23923  cnextcn  23936  qustgplem  23990  prdsmet  24239  blin2  24298  prdsbl  24360  nmolb  24586  tgqioo  24669  reconnlem2  24697  reconn  24698  lebnumlem3  24843  iscau4  25160  cmetcaulem  25169  iscmet3lem2  25173  bcthlem5  25209  minveclem3b  25309  pmltpc  25332  evthicc2  25342  ovolunlem2  25380  ovolicc2lem5  25403  mblsplit  25414  iundisj2  25431  volsup  25438  ioombl1lem4  25443  dyaddisj  25478  dyadmbllem  25481  i1faddlem  25575  itg10a  25592  itg1ge0a  25593  mbfi1flimlem  25604  mbfmullem  25607  itg2add  25641  rolle  25875  dvcvx  25906  itgsubst  25937  tdeglem4  25946  ply1domn  26010  fta1b  26058  plyadd  26103  plymul  26104  coeeu  26111  vieta1  26201  aalioulem6  26226  ulmcaulem  26284  ulmcau  26285  ulmbdd  26288  ulmcn  26289  amgm  26882  mumullem2  27071  ppiublem1  27094  dchrfi  27147  dchrptlem2  27157  dchrptlem3  27158  dchrsum2  27160  lgsdchr  27247  lgsquad2lem2  27277  2sqlem5  27314  2sqb  27324  pntlemp  27502  ostthlem2  27520  ostth  27531  nosupprefixmo  27593  noinfprefixmo  27594  noetasuplem4  27629  madebdaylemlrcut  27798  addsproplem2  27867  precsexlem11  28109  sltonold  28152  iscgrglt  28446  tgbtwnconn1  28507  colline  28581  lmimid  28726  axcontlem8  28903  axcontlem9  28904  eengtrkg  28918  numedglnl  29076  uhgr2edg  29140  uspgr2wlkeq  29578  wlkonl1iedg  29596  wlkdlem2  29614  pthdlem2  29700  clwlkclwwlklem2a4  29928  clwwisshclwwsn  29947  clwwlknon1sn  30031  frgr2wwlkeu  30258  frgrreg  30325  frgrregord013  30326  nvmul0or  30581  ubthlem3  30803  axhcompl-zf  30929  hvmul0or  30956  ocnel  31229  pjhthmo  31233  spanuni  31475  spansni  31488  hon0  31724  leopadd  32063  leoptr  32068  mdsymlem6  32339  sumdmdlem2  32350  cdjreui  32363  iundisj2f  32522  disjunsn  32526  iundisj2fi  32732  ballotlemimin  34487  bnj23  34698  bnj594  34892  bnj849  34905  setindregs  35078  cusgr3cyclex  35126  txsconn  35231  cvmsdisj  35260  cvmliftlem15  35288  cvmlift2lem10  35302  cvmlift3lem7  35315  fmla1  35377  satffunlem1lem2  35393  satffunlem2lem2  35396  mclsppslem  35573  dfon2lem3  35776  dfon2lem5  35778  dfon2lem6  35779  dfon2lem7  35780  dfon2lem8  35781  ifscgr  36035  cgr3tr4  36043  btwnconn1lem13  36090  seglecgr12  36102  elicc3  36308  neibastop1  36350  tailfb  36368  bj-sblem2  36834  bj-sngltag  36974  copsex2d  37130  mptsnunlem  37329  finxpreclem6  37387  wl-equsal1i  37535  lindsenlbs  37612  poimirlem26  37643  poimirlem27  37644  ismblfin  37658  itg2addnclem3  37670  ftc1anclem6  37695  fdc  37742  riscer  37985  intidl  38026  ispridlc  38067  disjlem14  38793  disjlem17  38794  prtlem14  38870  prtlem17  38872  lpssat  39009  lssatle  39011  lshpkrlem6  39111  cvrnbtwn  39267  atlatmstc  39315  atlatle  39316  atlrelat1  39317  2at0mat0  39521  trlator0  40167  cdleme0moN  40221  cdlemn11pre  41206  dihord2pre  41221  dihmeetlem20N  41322  dochkrshp4  41385  lcfl6  41496  expeqidd  42315  remullid  42424  diophin  42762  diophun  42763  inaex  44287  pm10.57  44361  modelaxreplem1  44968  fnchoice  45023  ellimcabssub0  45614  fourierdlem81  46182  fourierdlem93  46194  2reuimp0  47112  fzopredsuc  47321  2ffzoeq  47325  m1modmmod  47356  iccpartlt  47422  ichnreuop  47470  prmdvdsfmtnof1lem1  47582  lighneallem4  47608  odd2prm2  47716  even3prm2  47717  sbgoldbst  47776  nnsum4primesevenALTV  47799  stgrvtx0  47960  isubgr3stgrlem6  47969  grlimprclnbgrvtx  47997  pgnbgreunbgr  48123  ply1mulgsumlem1  48385  snlindsntor  48470  islininds2  48483  itschlc0xyqsol1  48765  2itscp  48780  opnneir  48905  iscnrm3lem2  48933