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  2944  rexlimdvvva  3196  spc2d  3571  pssdifn0  4334  ralnralall  4481  disjss3  5109  somo  5588  frminex  5620  sofld  6163  predtrss  6298  ordelord  6357  unizlim  6460  f0rn0  6748  funopfv  6913  mpteqb  6990  fvrnressn  7136  funfvima  7207  fpropnf1  7245  fliftfun  7290  weniso  7332  tfinds  7839  tfindsg  7840  tfindes  7842  tfinds2  7843  findsg  7876  resf1ext2b  7914  frxp  8108  poxp2  8125  soseq  8141  suppssr  8177  rdgsucmptnf  8400  frsucmptn  8410  tz7.49  8416  om00  8542  oewordi  8558  iiner  8765  eroveu  8788  fsetexb  8840  undomOLD  9034  sucdom2OLD  9056  sdomdif  9095  pssnn  9138  sucdom2  9173  php3  9179  unxpdomlem3  9206  fisseneq  9211  ordunifi  9244  isfinite2  9252  fiint  9284  fiintOLD  9285  infssuni  9304  ixpfi2  9308  finsschain  9317  ordtypelem10  9487  wofib  9505  wemapsolem  9510  unxpwdom2  9548  inf3lem2  9589  cantnfp1lem3  9640  cantnfp1  9641  setind  9694  frr3g  9716  r1tr  9736  r1ordg  9738  rankelb  9784  rankxplim3  9841  updjudhf  9891  cardlim  9932  infxpenlem  9973  infxpenc2  9982  dfac5lem4  10086  dfac5lem4OLD  10088  dfac12k  10108  kmlem13  10123  sornom  10237  fin23lem25  10284  fin23lem21  10299  zorn2lem4  10459  iundom2g  10500  fpwwe2lem11  10601  fpwwe2lem12  10602  pwfseqlem4a  10621  eltsk2g  10711  inttsk  10734  tskord  10740  r1tskina  10742  grudomon  10777  arch  12446  zaddcl  12580  uzm1  12838  xrsupsslem  13274  xrinfmsslem  13275  fsequb  13947  fseqsupubi  13950  ssnn0fi  13957  seqf1o  14015  sq01  14197  ccatalpha  14565  swrdnd0  14629  repsdf2  14750  cshw1  14794  wrdl3s3  14935  rexanre  15320  rexuzre  15326  cau3lem  15328  o1co  15559  rlimcn3  15563  o1of2  15586  lo1add  15600  lo1mul  15601  climcau  15644  climbdd  15645  caucvgb  15653  summo  15690  isumltss  15821  mertenslem2  15858  prodmolem2  15908  prodmo  15909  dvdsaddre2b  16284  bitsfzolem  16411  bitsfzo  16412  bezoutlem4  16519  lcmfeq0b  16607  lcmfunsnlem2  16617  divgcdcoprmex  16643  prmind2  16662  2mulprm  16670  isprm5  16684  prmdvdsbc  16703  prm23ge5  16793  pcqmul  16831  pcadd  16867  prmreclem2  16895  prmreclem5  16898  mul4sq  16932  vdwmc2  16957  ramcl  17007  prmgaplem7  17035  prmlem1a  17084  setsstruct2  17151  divsfval  17517  iscatd2  17649  catpropd  17677  wunfunc  17870  cyccom  19142  gaorber  19247  psgneu  19443  lsmsubm  19590  pj1eu  19633  efgredlem  19684  qusabl  19802  cygctb  19829  lt6abl  19832  gsumval3eu  19841  dprdsubg  19963  ablfac1c  20010  pgpfac1  20019  dvdsrtr  20284  unitgrp  20299  drngmul0orOLD  20677  abvn0b  20752  lvecvs0or  21025  lspdisjb  21043  lspsolvlem  21059  lspprat  21070  lbsextlem2  21076  nzerooringczr  21397  domnchr  21449  znfld  21477  cygznlem3  21486  obselocv  21644  cpmatacl  22610  chfacfisf  22748  chfacfisfcpmat  22749  0ntr  22965  opnneiid  23020  restntr  23076  hausnei2  23247  nrmsep3  23249  cmpsub  23294  uncmp  23297  dfconn2  23313  cnconn  23316  1stcfb  23339  txuni2  23459  txbas  23461  ptbasin  23471  txcls  23498  txbasval  23500  txlly  23530  txnlly  23531  pthaus  23532  txlm  23542  tx1stc  23544  xkohaus  23547  isufil2  23802  ufileu  23813  cnpflfi  23893  txflf  23900  fclscf  23919  flimfnfcls  23922  alexsubb  23940  alexsubALTlem2  23942  alexsubALTlem4  23944  ptcmplem2  23947  ptcmplem3  23948  cnextcn  23961  qustgplem  24015  prdsmet  24265  blin2  24324  prdsbl  24386  nmolb  24612  tgqioo  24695  reconnlem2  24723  reconn  24724  lebnumlem3  24869  iscau4  25186  cmetcaulem  25195  iscmet3lem2  25199  bcthlem5  25235  minveclem3b  25335  pmltpc  25358  evthicc2  25368  ovolunlem2  25406  ovolicc2lem5  25429  mblsplit  25440  iundisj2  25457  volsup  25464  ioombl1lem4  25469  dyaddisj  25504  dyadmbllem  25507  i1faddlem  25601  itg10a  25618  itg1ge0a  25619  mbfi1flimlem  25630  mbfmullem  25633  itg2add  25667  rolle  25901  dvcvx  25932  itgsubst  25963  tdeglem4  25972  ply1domn  26036  fta1b  26084  plyadd  26129  plymul  26130  coeeu  26137  vieta1  26227  aalioulem6  26252  ulmcaulem  26310  ulmcau  26311  ulmbdd  26314  ulmcn  26315  amgm  26908  mumullem2  27097  ppiublem1  27120  dchrfi  27173  dchrptlem2  27183  dchrptlem3  27184  dchrsum2  27186  lgsdchr  27273  lgsquad2lem2  27303  2sqlem5  27340  2sqb  27350  pntlemp  27528  ostthlem2  27546  ostth  27557  nosupprefixmo  27619  noinfprefixmo  27620  noetasuplem4  27655  madebdaylemlrcut  27817  addsproplem2  27884  precsexlem11  28126  sltonold  28169  iscgrglt  28448  tgbtwnconn1  28509  colline  28583  lmimid  28728  axcontlem8  28905  axcontlem9  28906  eengtrkg  28920  numedglnl  29078  uhgr2edg  29142  uspgr2wlkeq  29581  wlkonl1iedg  29600  wlkdlem2  29618  pthdlem2  29705  clwlkclwwlklem2a4  29933  clwwisshclwwsn  29952  clwwlknon1sn  30036  frgr2wwlkeu  30263  frgrreg  30330  frgrregord013  30331  nvmul0or  30586  ubthlem3  30808  axhcompl-zf  30934  hvmul0or  30961  ocnel  31234  pjhthmo  31238  spanuni  31480  spansni  31493  hon0  31729  leopadd  32068  leoptr  32073  mdsymlem6  32344  sumdmdlem2  32355  cdjreui  32368  iundisj2f  32526  disjunsn  32530  iundisj2fi  32727  ballotlemimin  34504  bnj23  34715  bnj594  34909  bnj849  34922  cusgr3cyclex  35130  txsconn  35235  cvmsdisj  35264  cvmliftlem15  35292  cvmlift2lem10  35306  cvmlift3lem7  35319  fmla1  35381  satffunlem1lem2  35397  satffunlem2lem2  35400  mclsppslem  35577  dfon2lem3  35780  dfon2lem5  35782  dfon2lem6  35783  dfon2lem7  35784  dfon2lem8  35785  ifscgr  36039  cgr3tr4  36047  btwnconn1lem13  36094  seglecgr12  36106  elicc3  36312  neibastop1  36354  tailfb  36372  bj-sblem2  36838  bj-sngltag  36978  copsex2d  37134  mptsnunlem  37333  finxpreclem6  37391  wl-equsal1i  37539  lindsenlbs  37616  poimirlem26  37647  poimirlem27  37648  ismblfin  37662  itg2addnclem3  37674  ftc1anclem6  37699  fdc  37746  riscer  37989  intidl  38030  ispridlc  38071  disjlem14  38797  disjlem17  38798  prtlem14  38874  prtlem17  38876  lpssat  39013  lssatle  39015  lshpkrlem6  39115  cvrnbtwn  39271  atlatmstc  39319  atlatle  39320  atlrelat1  39321  2at0mat0  39526  trlator0  40172  cdleme0moN  40226  cdlemn11pre  41211  dihord2pre  41226  dihmeetlem20N  41327  dochkrshp4  41390  lcfl6  41501  expeqidd  42320  remullid  42429  diophin  42767  diophun  42768  inaex  44293  pm10.57  44367  modelaxreplem1  44975  fnchoice  45030  ellimcabssub0  45622  fourierdlem81  46192  fourierdlem93  46204  2reuimp0  47119  fzopredsuc  47328  2ffzoeq  47332  m1modmmod  47363  iccpartlt  47429  ichnreuop  47477  prmdvdsfmtnof1lem1  47589  lighneallem4  47615  odd2prm2  47723  even3prm2  47724  sbgoldbst  47783  nnsum4primesevenALTV  47806  stgrvtx0  47965  isubgr3stgrlem6  47974  pgnbgreunbgr  48119  ply1mulgsumlem1  48379  snlindsntor  48464  islininds2  48477  itschlc0xyqsol1  48759  2itscp  48774  opnneir  48899  iscnrm3lem2  48927