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  1674  19.30  1882  19.33b  1886  necon1bd  2948  rexlimdvvva  3192  spc2d  3554  pssdifn0  4318  ralnralall  4464  disjss3  5095  somo  5569  frminex  5601  sofld  6143  predtrss  6278  ordelord  6337  unizlim  6439  f0rn0  6717  funopfv  6881  mpteqb  6958  fvrnressn  7104  funfvima  7174  fpropnf1  7211  fliftfun  7256  weniso  7298  tfinds  7800  tfindsg  7801  tfindes  7803  tfinds2  7804  findsg  7837  resf1ext2b  7875  frxp  8066  poxp2  8083  soseq  8099  suppssr  8135  rdgsucmptnf  8358  frsucmptn  8368  tz7.49  8374  om00  8500  oewordi  8517  iiner  8724  eroveu  8747  fsetexb  8799  sdomdif  9051  pssnn  9091  sucdom2  9125  php3  9131  unxpdomlem3  9156  fisseneq  9161  ordunifi  9188  isfinite2  9196  fiint  9225  infssuni  9244  ixpfi2  9248  finsschain  9257  ordtypelem10  9430  wofib  9448  wemapsolem  9453  unxpwdom2  9491  inf3lem2  9536  cantnfp1lem3  9587  cantnfp1  9588  setind  9654  frr3g  9666  r1tr  9686  r1ordg  9688  rankelb  9734  rankxplim3  9791  updjudhf  9841  cardlim  9882  infxpenlem  9921  infxpenc2  9930  dfac5lem4  10034  dfac5lem4OLD  10036  dfac12k  10056  kmlem13  10071  sornom  10185  fin23lem25  10232  fin23lem21  10247  zorn2lem4  10407  iundom2g  10448  fpwwe2lem11  10550  fpwwe2lem12  10551  pwfseqlem4a  10570  eltsk2g  10660  inttsk  10683  tskord  10689  r1tskina  10691  grudomon  10726  arch  12396  zaddcl  12529  uzm1  12783  xrsupsslem  13220  xrinfmsslem  13221  fsequb  13896  fseqsupubi  13899  ssnn0fi  13906  seqf1o  13964  sq01  14146  ccatalpha  14515  swrdnd0  14579  repsdf2  14699  cshw1  14743  wrdl3s3  14883  rexanre  15268  rexuzre  15274  cau3lem  15276  o1co  15507  rlimcn3  15511  o1of2  15534  lo1add  15548  lo1mul  15549  climcau  15592  climbdd  15593  caucvgb  15601  summo  15638  isumltss  15769  mertenslem2  15806  prodmolem2  15856  prodmo  15857  dvdsaddre2b  16232  bitsfzolem  16359  bitsfzo  16360  bezoutlem4  16467  lcmfeq0b  16555  lcmfunsnlem2  16565  divgcdcoprmex  16591  prmind2  16610  2mulprm  16618  isprm5  16632  prmdvdsbc  16651  prm23ge5  16741  pcqmul  16779  pcadd  16815  prmreclem2  16843  prmreclem5  16846  mul4sq  16880  vdwmc2  16905  ramcl  16955  prmgaplem7  16983  prmlem1a  17032  setsstruct2  17099  divsfval  17466  iscatd2  17602  catpropd  17630  wunfunc  17823  cyccom  19130  gaorber  19235  psgneu  19433  lsmsubm  19580  pj1eu  19623  efgredlem  19674  qusabl  19792  cygctb  19819  lt6abl  19822  gsumval3eu  19831  dprdsubg  19953  ablfac1c  20000  pgpfac1  20009  dvdsrtr  20302  unitgrp  20317  drngmul0orOLD  20692  abvn0b  20767  lvecvs0or  21061  lspdisjb  21079  lspsolvlem  21095  lspprat  21106  lbsextlem2  21112  nzerooringczr  21433  domnchr  21485  znfld  21513  cygznlem3  21522  obselocv  21681  cpmatacl  22658  chfacfisf  22796  chfacfisfcpmat  22797  0ntr  23013  opnneiid  23068  restntr  23124  hausnei2  23295  nrmsep3  23297  cmpsub  23342  uncmp  23345  dfconn2  23361  cnconn  23364  1stcfb  23387  txuni2  23507  txbas  23509  ptbasin  23519  txcls  23546  txbasval  23548  txlly  23578  txnlly  23579  pthaus  23580  txlm  23590  tx1stc  23592  xkohaus  23595  isufil2  23850  ufileu  23861  cnpflfi  23941  txflf  23948  fclscf  23967  flimfnfcls  23970  alexsubb  23988  alexsubALTlem2  23990  alexsubALTlem4  23992  ptcmplem2  23995  ptcmplem3  23996  cnextcn  24009  qustgplem  24063  prdsmet  24312  blin2  24371  prdsbl  24433  nmolb  24659  tgqioo  24742  reconnlem2  24770  reconn  24771  lebnumlem3  24916  iscau4  25233  cmetcaulem  25242  iscmet3lem2  25246  bcthlem5  25282  minveclem3b  25382  pmltpc  25405  evthicc2  25415  ovolunlem2  25453  ovolicc2lem5  25476  mblsplit  25487  iundisj2  25504  volsup  25511  ioombl1lem4  25516  dyaddisj  25551  dyadmbllem  25554  i1faddlem  25648  itg10a  25665  itg1ge0a  25666  mbfi1flimlem  25677  mbfmullem  25680  itg2add  25714  rolle  25948  dvcvx  25979  itgsubst  26010  tdeglem4  26019  ply1domn  26083  fta1b  26131  plyadd  26176  plymul  26177  coeeu  26184  vieta1  26274  aalioulem6  26299  ulmcaulem  26357  ulmcau  26358  ulmbdd  26361  ulmcn  26362  amgm  26955  mumullem2  27144  ppiublem1  27167  dchrfi  27220  dchrptlem2  27230  dchrptlem3  27231  dchrsum2  27233  lgsdchr  27320  lgsquad2lem2  27350  2sqlem5  27387  2sqb  27397  pntlemp  27575  ostthlem2  27593  ostth  27604  nosupprefixmo  27666  noinfprefixmo  27667  noetasuplem4  27702  madebdaylemlrcut  27871  addsproplem2  27940  precsexlem11  28185  sltonold  28229  iscgrglt  28535  tgbtwnconn1  28596  colline  28670  lmimid  28815  axcontlem8  28993  axcontlem9  28994  eengtrkg  29008  numedglnl  29166  uhgr2edg  29230  uspgr2wlkeq  29668  wlkonl1iedg  29686  wlkdlem2  29704  pthdlem2  29790  clwlkclwwlklem2a4  30021  clwwisshclwwsn  30040  clwwlknon1sn  30124  frgr2wwlkeu  30351  frgrreg  30418  frgrregord013  30419  nvmul0or  30674  ubthlem3  30896  axhcompl-zf  31022  hvmul0or  31049  ocnel  31322  pjhthmo  31326  spanuni  31568  spansni  31581  hon0  31817  leopadd  32156  leoptr  32161  mdsymlem6  32432  sumdmdlem2  32443  cdjreui  32456  iundisj2f  32614  disjunsn  32618  iundisj2fi  32826  ballotlemimin  34612  bnj23  34823  bnj594  35017  bnj849  35030  setindregs  35235  cusgr3cyclex  35279  txsconn  35384  cvmsdisj  35413  cvmliftlem15  35441  cvmlift2lem10  35455  cvmlift3lem7  35468  fmla1  35530  satffunlem1lem2  35546  satffunlem2lem2  35549  mclsppslem  35726  dfon2lem3  35926  dfon2lem5  35928  dfon2lem6  35929  dfon2lem7  35930  dfon2lem8  35931  ifscgr  36187  cgr3tr4  36195  btwnconn1lem13  36242  seglecgr12  36254  elicc3  36460  neibastop1  36502  tailfb  36520  bj-sblem2  36987  bj-sngltag  37127  copsex2d  37283  mptsnunlem  37482  finxpreclem6  37540  wl-equsal1i  37688  lindsenlbs  37755  poimirlem26  37786  poimirlem27  37787  ismblfin  37801  itg2addnclem3  37813  ftc1anclem6  37838  fdc  37885  riscer  38128  intidl  38169  ispridlc  38210  disjlem14  38996  disjlem17  38997  prtlem14  39073  prtlem17  39075  lpssat  39212  lssatle  39214  lshpkrlem6  39314  cvrnbtwn  39470  atlatmstc  39518  atlatle  39519  atlrelat1  39520  2at0mat0  39724  trlator0  40370  cdleme0moN  40424  cdlemn11pre  41409  dihord2pre  41424  dihmeetlem20N  41525  dochkrshp4  41588  lcfl6  41699  expeqidd  42522  remullid  42631  diophin  42956  diophun  42957  inaex  44480  pm10.57  44554  modelaxreplem1  45161  fnchoice  45216  ellimcabssub0  45805  fourierdlem81  46373  fourierdlem93  46385  2reuimp0  47302  fzopredsuc  47511  2ffzoeq  47515  m1modmmod  47546  iccpartlt  47612  ichnreuop  47660  prmdvdsfmtnof1lem1  47772  lighneallem4  47798  odd2prm2  47906  even3prm2  47907  sbgoldbst  47966  nnsum4primesevenALTV  47989  stgrvtx0  48150  isubgr3stgrlem6  48159  grlimprclnbgrvtx  48187  pgnbgreunbgr  48313  ply1mulgsumlem1  48574  snlindsntor  48659  islininds2  48672  itschlc0xyqsol1  48954  2itscp  48969  opnneir  49094  iscnrm3lem2  49122