Theorem biimtrrid 246

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3imtr3g  298  oplem1  1072  nic-ax  1705  19.30  1913  19.33b  1917  sbrimvw  2127  necon1bd  2973  rexlimdvvva  3220  spc2d  3556  pssdifn0  4315  ralnralall  4468  disjss3  5101  somo  5598  frminex  5630  sofld  6181  predtrss  6328  ordelord  6387  unizlim  6490  f0rn0  6772  funopfv  6939  mpteqb  7018  fvrnressn  7170  funfvima  7240  fpropnf1  7275  fliftfun  7324  weniso  7368  tfinds  7875  tfindsg  7876  tfindes  7878  tfinds2  7879  findsg  7913  resf1ext2b  7951  frxp  8145  poxp2  8167  soseq  8183  suppssr  8220  rdgsucmptnf  8445  frsucmptn  8455  tz7.49  8463  om00  8591  oewordi  8608  iiner  8818  eroveu  8841  fsetexb  8894  sdomdif  9152  pssnn  9192  sucdom2  9226  php3  9232  unxpdomlem3  9257  fisseneq  9262  ordunifi  9289  isfinite2  9298  fiint  9326  infssuni  9343  ixpfi2  9347  finsschain  9356  ordtypelem10  9528  wofib  9546  wemapsolem  9551  unxpwdom2  9589  inf3lem2  9637  cantnfp1lem3  9688  cantnfp1  9689  setind  9755  frr3g  9767  r1tr  9790  r1ordg  9792  rankelb  9840  rankxplim3  9905  updjudhf  10019  cardlim  10060  infxpenlem  10099  infxpenc2  10108  dfac5lem4  10212  dfac12k  10233  kmlem13  10248  sornom  10362  fin23lem25  10409  fin23lem21  10424  zorn2lem4  10584  iundom2g  10631  fpwwe2lem11  10733  fpwwe2lem12  10734  pwfseqlem4a  10753  eltsk2g  10843  inttsk  10866  tskord  10872  r1tskina  10874  grudomon  10909  arch  12610  zaddcl  12743  uzm1  13006  xrsupsslem  13444  xrinfmsslem  13445  fsequb  14125  fseqsupubi  14128  ssnn0fi  14135  seqf1o  14193  sq01  14376  ccatalpha  14747  swrdnd0  14815  repsdf2  14937  cshw1  14981  wrdl3s3  15124  rexanre  15523  rexuzre  15529  cau3lem  15531  o1co  15762  rlimcn3  15766  o1of2  15789  lo1add  15803  lo1mul  15804  climcau  15847  climbdd  15848  caucvgb  15856  summo  15892  isumltss  16026  mertenslem2  16063  prodmolem2  16111  prodmo  16112  dvdsaddre2b  16486  bitsfzolem  16613  bitsfzo  16614  bezoutlem4  16724  lcmfeq0b  16814  lcmfunsnlem2  16824  divgcdcoprmex  16850  prmind2  16869  2mulprm  16877  isprm5  16892  prmdvdsbc  16911  prm23ge5  17002  pcqmul  17040  pcadd  17076  prmreclem2  17104  prmreclem5  17107  mul4sq  17141  vdwmc2  17166  ramcl  17216  prmgaplem7  17244  prmlem1a  17293  setsstruct2  17361  divsfval  17728  iscatd2  17864  catpropd  17892  wunfunc  18085  cyccom  19427  gaorber  19531  psgneu  19729  lsmsubm  19876  pj1eu  19919  efgredlem  19970  qusabl  20088  cygctb  20115  lt6abl  20118  gsumval3eu  20127  dprdsubg  20249  ablfac1c  20296  pgpfac1  20305  dvdsrtr  20607  unitgrp  20622  abvn0b  21102  lvecvs0or  21395  lspdisjb  21413  lspsolvlem  21429  lspprat  21440  lbsextlem2  21446  nzerooringczr  21795  domnchr  21847  znfld  21875  cygznlem3  21884  obselocv  22043  lindsenlbs  22166  cpmatacl  23043  chfacfisf  23181  chfacfisfcpmat  23182  0ntr  23398  opnneiid  23453  restntr  23509  hausnei2  23680  nrmsep3  23682  cmpsub  23727  uncmp  23730  dfconn2  23746  cnconn  23749  1stcfb  23772  txuni2  23893  txbas  23895  ptbasin  23905  txcls  23932  txbasval  23934  txlly  23964  txnlly  23965  pthaus  23966  txlm  23976  tx1stc  23978  xkohaus  23981  isufil2  24236  ufileu  24247  cnpflfi  24327  txflf  24334  fclscf  24353  flimfnfcls  24356  alexsubb  24374  alexsubALTlem2  24376  alexsubALTlem4  24378  ptcmplem2  24381  ptcmplem3  24382  cnextcn  24395  qustgplem  24449  prdsmet  24698  blin2  24757  prdsbl  24819  nmolb  25045  tgqioo  25128  reconnlem2  25156  reconn  25157  lebnumlem3  25293  iscau4  25609  cmetcaulem  25618  iscmet3lem2  25622  bcthlem5  25658  minveclem3b  25758  pmltpc  25780  evthicc2  25790  ovolunlem2  25828  ovolicc2lem5  25851  mblsplit  25862  iundisj2  25879  volsup  25886  ioombl1lem4  25891  dyaddisj  25926  dyadmbllem  25929  i1faddlem  26023  itg10a  26040  itg1ge0a  26041  mbfi1flimlem  26052  mbfmullem  26055  itg2add  26089  rolle  26319  dvcvx  26349  itgsubst  26378  tdeglem4  26387  ply1domn  26451  fta1b  26499  plyadd  26545  plymul  26546  coeeu  26553  vieta1  26644  aalioulem6  26673  ulmcaulem  26730  ulmcau  26731  ulmbdd  26734  ulmcn  26735  amgm  27327  mumullem2  27516  ppiublem1  27538  dchrfi  27591  dchrptlem2  27601  dchrptlem3  27602  dchrsum2  27604  lgsdchr  27691  lgsquad2lem2  27721  2sqlem5  27758  2sqb  27768  pntlemp  27946  ostthlem2  27964  ostth  27975  nosupprefixmo  28066  noinfprefixmo  28067  noetasuplem4  28102  madebdaylemlrcut  28294  addsproplem2  28365  precsexlem11  28612  ltonold  28656  bdayfinbndlem1  28862  iscgrglt  28986  tgbtwnconn1  29047  colline  29127  lmimid  29308  axcontlem8  29558  axcontlem9  29559  eengtrkg  29573  numedglnl  29731  uhgr2edg  29798  uspgr2wlkeq  30235  wlkonl1iedg  30253  wlkdlem2  30271  pthdlem2  30363  clwlkclwwlklem2a4  30597  clwwisshclwwsn  30616  clwwlknon1sn  30700  frgr2wwlkeu  30937  frgrreg  31004  frgrregord013  31005  nvmul0or  31261  ubthlem3  31483  axhcompl-zf  31609  hvmul0or  31636  ocnel  31909  pjhthmo  31913  spanuni  32155  spansni  32168  hon0  32404  leopadd  32743  leoptr  32748  mdsymlem6  33019  sumdmdlem2  33030  cdjreui  33043  iundisj2f  33235  disjunsn  33239  iundisj2fi  33439  ballotlemimin  35188  bnj23  35399  bnj594  35592  bnj849  35605  setindregs  35866  karddom  35897  kardsdom  35898  j00smo  35956  cusgr3cyclex  36019  txsconn  36124  cvmsdisj  36153  cvmliftlem15  36181  cvmlift2lem10  36195  cvmlift3lem7  36208  fmla1  36270  satffunlem1lem2  36286  satffunlem2lem2  36289  mclsppslem  36466  dfon2lem3  36671  dfon2lem5  36673  dfon2lem6  36674  dfon2lem7  36675  dfon2lem8  36676  ifscgr  36933  cgr3tr4  36941  btwnconn1lem13  36988  seglecgr12  37000  elicc3  37229  neibastop1  37271  tailfb  37289  bj-sblem2  37879  bj-sngltag  38020  copsex2d  38197  mptsnunlem  38398  finxpreclem6  38456  wl-equsal1i  38613  poimirlem26  38701  poimirlem27  38702  ismblfin  38716  itg2addnclem3  38728  ftc1anclem6  38753  fdc  38816  riscer  39059  intidl  39100  ispridlc  39141  disjlem14  39970  disjlem17  39971  prtlem14  40068  prtlem17  40070  lpssat  40207  lssatle  40209  lshpkrlem6  40309  cvrnbtwn  40465  atlatmstc  40513  atlatle  40514  atlrelat1  40515  2at0mat0  40719  trlator0  41365  cdleme0moN  41419  cdlemn11pre  42404  dihord2pre  42419  dihmeetlem20N  42520  dochkrshp4  42583  lcfl6  42694  expeqidd  43519  remullid  43622  diophin  43920  diophun  43921  inaex  45418  pm10.57  45492  modelaxreplem1  46104  fnchoice  46182  ellimcabssub0  46765  fourierdlem81  47333  fourierdlem93  47345  2reuimp0  48321  fzopredsuc  48530  2ffzoeq  48534  m1modmmod  48570  iccpartlt  48642  ichnreuop  48690  prmdvdsfmtnof1lem1  48805  lighneallem4  48831  odd2prm2  48952  even3prm2  48953  sbgoldbst  49012  nnsum4primesevenALTV  49035  stgrvtx0  49196  isubgr3stgrlem6  49205  grlimprclnbgrvtx  49233  pgnbgreunbgr  49359  ply1mulgsumlem1  49634  snlindsntor  49719  islininds2  49732  itschlc0xyqsol1  50014  2itscp  50029  opnneir  50157  iscnrm3lem2  50185