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  2951  rexlimdvvva  3196  spc2d  3545  pssdifn0  4309  ralnralall  4454  disjss3  5085  somo  5572  frminex  5604  sofld  6146  predtrss  6281  ordelord  6340  unizlim  6442  f0rn0  6720  funopfv  6884  mpteqb  6962  fvrnressn  7109  funfvima  7179  fpropnf1  7216  fliftfun  7261  weniso  7303  tfinds  7805  tfindsg  7806  tfindes  7808  tfinds2  7809  findsg  7842  resf1ext2b  7880  frxp  8070  poxp2  8087  soseq  8103  suppssr  8139  rdgsucmptnf  8362  frsucmptn  8372  tz7.49  8378  om00  8504  oewordi  8521  iiner  8730  eroveu  8753  fsetexb  8805  sdomdif  9057  pssnn  9097  sucdom2  9131  php3  9137  unxpdomlem3  9162  fisseneq  9167  ordunifi  9194  isfinite2  9202  fiint  9231  infssuni  9250  ixpfi2  9254  finsschain  9263  ordtypelem10  9436  wofib  9454  wemapsolem  9459  unxpwdom2  9497  inf3lem2  9544  cantnfp1lem3  9595  cantnfp1  9596  setind  9662  frr3g  9674  r1tr  9694  r1ordg  9696  rankelb  9742  rankxplim3  9799  updjudhf  9849  cardlim  9890  infxpenlem  9929  infxpenc2  9938  dfac5lem4  10042  dfac5lem4OLD  10044  dfac12k  10064  kmlem13  10079  sornom  10193  fin23lem25  10240  fin23lem21  10255  zorn2lem4  10415  iundom2g  10456  fpwwe2lem11  10558  fpwwe2lem12  10559  pwfseqlem4a  10578  eltsk2g  10668  inttsk  10691  tskord  10697  r1tskina  10699  grudomon  10734  arch  12428  zaddcl  12561  uzm1  12816  xrsupsslem  13253  xrinfmsslem  13254  fsequb  13931  fseqsupubi  13934  ssnn0fi  13941  seqf1o  13999  sq01  14181  ccatalpha  14550  swrdnd0  14614  repsdf2  14734  cshw1  14778  wrdl3s3  14918  rexanre  15303  rexuzre  15309  cau3lem  15311  o1co  15542  rlimcn3  15546  o1of2  15569  lo1add  15583  lo1mul  15584  climcau  15627  climbdd  15628  caucvgb  15636  summo  15673  isumltss  15807  mertenslem2  15844  prodmolem2  15894  prodmo  15895  dvdsaddre2b  16270  bitsfzolem  16397  bitsfzo  16398  bezoutlem4  16505  lcmfeq0b  16593  lcmfunsnlem2  16603  divgcdcoprmex  16629  prmind2  16648  2mulprm  16656  isprm5  16671  prmdvdsbc  16690  prm23ge5  16780  pcqmul  16818  pcadd  16854  prmreclem2  16882  prmreclem5  16885  mul4sq  16919  vdwmc2  16944  ramcl  16994  prmgaplem7  17022  prmlem1a  17071  setsstruct2  17138  divsfval  17505  iscatd2  17641  catpropd  17669  wunfunc  17862  cyccom  19172  gaorber  19277  psgneu  19475  lsmsubm  19622  pj1eu  19665  efgredlem  19716  qusabl  19834  cygctb  19861  lt6abl  19864  gsumval3eu  19873  dprdsubg  19995  ablfac1c  20042  pgpfac1  20051  dvdsrtr  20342  unitgrp  20357  drngmul0orOLD  20732  abvn0b  20807  lvecvs0or  21101  lspdisjb  21119  lspsolvlem  21135  lspprat  21146  lbsextlem2  21152  nzerooringczr  21473  domnchr  21525  znfld  21553  cygznlem3  21562  obselocv  21721  cpmatacl  22694  chfacfisf  22832  chfacfisfcpmat  22833  0ntr  23049  opnneiid  23104  restntr  23160  hausnei2  23331  nrmsep3  23333  cmpsub  23378  uncmp  23381  dfconn2  23397  cnconn  23400  1stcfb  23423  txuni2  23543  txbas  23545  ptbasin  23555  txcls  23582  txbasval  23584  txlly  23614  txnlly  23615  pthaus  23616  txlm  23626  tx1stc  23628  xkohaus  23631  isufil2  23886  ufileu  23897  cnpflfi  23977  txflf  23984  fclscf  24003  flimfnfcls  24006  alexsubb  24024  alexsubALTlem2  24026  alexsubALTlem4  24028  ptcmplem2  24031  ptcmplem3  24032  cnextcn  24045  qustgplem  24099  prdsmet  24348  blin2  24407  prdsbl  24469  nmolb  24695  tgqioo  24778  reconnlem2  24806  reconn  24807  lebnumlem3  24943  iscau4  25259  cmetcaulem  25268  iscmet3lem2  25272  bcthlem5  25308  minveclem3b  25408  pmltpc  25430  evthicc2  25440  ovolunlem2  25478  ovolicc2lem5  25501  mblsplit  25512  iundisj2  25529  volsup  25536  ioombl1lem4  25541  dyaddisj  25576  dyadmbllem  25579  i1faddlem  25673  itg10a  25690  itg1ge0a  25691  mbfi1flimlem  25702  mbfmullem  25705  itg2add  25739  rolle  25970  dvcvx  26000  itgsubst  26029  tdeglem4  26038  ply1domn  26102  fta1b  26150  plyadd  26195  plymul  26196  coeeu  26203  vieta1  26292  aalioulem6  26317  ulmcaulem  26375  ulmcau  26376  ulmbdd  26379  ulmcn  26380  amgm  26971  mumullem2  27160  ppiublem1  27182  dchrfi  27235  dchrptlem2  27245  dchrptlem3  27246  dchrsum2  27248  lgsdchr  27335  lgsquad2lem2  27365  2sqlem5  27402  2sqb  27412  pntlemp  27590  ostthlem2  27608  ostth  27619  nosupprefixmo  27681  noinfprefixmo  27682  noetasuplem4  27717  madebdaylemlrcut  27908  addsproplem2  27979  precsexlem11  28226  ltonold  28270  bdayfinbndlem1  28476  iscgrglt  28599  tgbtwnconn1  28660  colline  28734  lmimid  28879  axcontlem8  29057  axcontlem9  29058  eengtrkg  29072  numedglnl  29230  uhgr2edg  29294  uspgr2wlkeq  29732  wlkonl1iedg  29750  wlkdlem2  29768  pthdlem2  29854  clwlkclwwlklem2a4  30085  clwwisshclwwsn  30104  clwwlknon1sn  30188  frgr2wwlkeu  30415  frgrreg  30482  frgrregord013  30483  nvmul0or  30739  ubthlem3  30961  axhcompl-zf  31087  hvmul0or  31114  ocnel  31387  pjhthmo  31391  spanuni  31633  spansni  31646  hon0  31882  leopadd  32221  leoptr  32226  mdsymlem6  32497  sumdmdlem2  32508  cdjreui  32521  iundisj2f  32678  disjunsn  32682  iundisj2fi  32888  ballotlemimin  34669  bnj23  34880  bnj594  35073  bnj849  35086  setindregs  35293  cusgr3cyclex  35337  txsconn  35442  cvmsdisj  35471  cvmliftlem15  35499  cvmlift2lem10  35513  cvmlift3lem7  35526  fmla1  35588  satffunlem1lem2  35604  satffunlem2lem2  35607  mclsppslem  35784  dfon2lem3  35984  dfon2lem5  35986  dfon2lem6  35987  dfon2lem7  35988  dfon2lem8  35989  ifscgr  36245  cgr3tr4  36253  btwnconn1lem13  36300  seglecgr12  36312  elicc3  36518  neibastop1  36560  tailfb  36578  bj-sblem2  37169  bj-sngltag  37309  copsex2d  37472  mptsnunlem  37671  finxpreclem6  37729  wl-equsal1i  37886  lindsenlbs  37953  poimirlem26  37984  poimirlem27  37985  ismblfin  37999  itg2addnclem3  38011  ftc1anclem6  38036  fdc  38083  riscer  38326  intidl  38367  ispridlc  38408  disjlem14  39239  disjlem17  39240  prtlem14  39337  prtlem17  39339  lpssat  39476  lssatle  39478  lshpkrlem6  39578  cvrnbtwn  39734  atlatmstc  39782  atlatle  39783  atlrelat1  39784  2at0mat0  39988  trlator0  40634  cdleme0moN  40688  cdlemn11pre  41673  dihord2pre  41688  dihmeetlem20N  41789  dochkrshp4  41852  lcfl6  41963  expeqidd  42774  remullid  42883  diophin  43221  diophun  43222  inaex  44745  pm10.57  44819  modelaxreplem1  45426  fnchoice  45481  ellimcabssub0  46068  fourierdlem81  46636  fourierdlem93  46648  2reuimp0  47577  fzopredsuc  47787  2ffzoeq  47791  m1modmmod  47827  iccpartlt  47899  ichnreuop  47947  prmdvdsfmtnof1lem1  48062  lighneallem4  48088  odd2prm2  48209  even3prm2  48210  sbgoldbst  48269  nnsum4primesevenALTV  48292  stgrvtx0  48453  isubgr3stgrlem6  48462  grlimprclnbgrvtx  48490  pgnbgreunbgr  48616  ply1mulgsumlem1  48877  snlindsntor  48962  islininds2  48975  itschlc0xyqsol1  49257  2itscp  49272  opnneir  49397  iscnrm3lem2  49425