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  2950  rexlimdvvva  3194  spc2d  3556  pssdifn0  4320  ralnralall  4466  disjss3  5097  somo  5571  frminex  5603  sofld  6145  predtrss  6280  ordelord  6339  unizlim  6441  f0rn0  6719  funopfv  6883  mpteqb  6960  fvrnressn  7106  funfvima  7176  fpropnf1  7213  fliftfun  7258  weniso  7300  tfinds  7802  tfindsg  7803  tfindes  7805  tfinds2  7806  findsg  7839  resf1ext2b  7877  frxp  8068  poxp2  8085  soseq  8101  suppssr  8137  rdgsucmptnf  8360  frsucmptn  8370  tz7.49  8376  om00  8502  oewordi  8519  iiner  8726  eroveu  8749  fsetexb  8801  sdomdif  9053  pssnn  9093  sucdom2  9127  php3  9133  unxpdomlem3  9158  fisseneq  9163  ordunifi  9190  isfinite2  9198  fiint  9227  infssuni  9246  ixpfi2  9250  finsschain  9259  ordtypelem10  9432  wofib  9450  wemapsolem  9455  unxpwdom2  9493  inf3lem2  9538  cantnfp1lem3  9589  cantnfp1  9590  setind  9656  frr3g  9668  r1tr  9688  r1ordg  9690  rankelb  9736  rankxplim3  9793  updjudhf  9843  cardlim  9884  infxpenlem  9923  infxpenc2  9932  dfac5lem4  10036  dfac5lem4OLD  10038  dfac12k  10058  kmlem13  10073  sornom  10187  fin23lem25  10234  fin23lem21  10249  zorn2lem4  10409  iundom2g  10450  fpwwe2lem11  10552  fpwwe2lem12  10553  pwfseqlem4a  10572  eltsk2g  10662  inttsk  10685  tskord  10691  r1tskina  10693  grudomon  10728  arch  12398  zaddcl  12531  uzm1  12785  xrsupsslem  13222  xrinfmsslem  13223  fsequb  13898  fseqsupubi  13901  ssnn0fi  13908  seqf1o  13966  sq01  14148  ccatalpha  14517  swrdnd0  14581  repsdf2  14701  cshw1  14745  wrdl3s3  14885  rexanre  15270  rexuzre  15276  cau3lem  15278  o1co  15509  rlimcn3  15513  o1of2  15536  lo1add  15550  lo1mul  15551  climcau  15594  climbdd  15595  caucvgb  15603  summo  15640  isumltss  15771  mertenslem2  15808  prodmolem2  15858  prodmo  15859  dvdsaddre2b  16234  bitsfzolem  16361  bitsfzo  16362  bezoutlem4  16469  lcmfeq0b  16557  lcmfunsnlem2  16567  divgcdcoprmex  16593  prmind2  16612  2mulprm  16620  isprm5  16634  prmdvdsbc  16653  prm23ge5  16743  pcqmul  16781  pcadd  16817  prmreclem2  16845  prmreclem5  16848  mul4sq  16882  vdwmc2  16907  ramcl  16957  prmgaplem7  16985  prmlem1a  17034  setsstruct2  17101  divsfval  17468  iscatd2  17604  catpropd  17632  wunfunc  17825  cyccom  19132  gaorber  19237  psgneu  19435  lsmsubm  19582  pj1eu  19625  efgredlem  19676  qusabl  19794  cygctb  19821  lt6abl  19824  gsumval3eu  19833  dprdsubg  19955  ablfac1c  20002  pgpfac1  20011  dvdsrtr  20304  unitgrp  20319  drngmul0orOLD  20694  abvn0b  20769  lvecvs0or  21063  lspdisjb  21081  lspsolvlem  21097  lspprat  21108  lbsextlem2  21114  nzerooringczr  21435  domnchr  21487  znfld  21515  cygznlem3  21524  obselocv  21683  cpmatacl  22660  chfacfisf  22798  chfacfisfcpmat  22799  0ntr  23015  opnneiid  23070  restntr  23126  hausnei2  23297  nrmsep3  23299  cmpsub  23344  uncmp  23347  dfconn2  23363  cnconn  23366  1stcfb  23389  txuni2  23509  txbas  23511  ptbasin  23521  txcls  23548  txbasval  23550  txlly  23580  txnlly  23581  pthaus  23582  txlm  23592  tx1stc  23594  xkohaus  23597  isufil2  23852  ufileu  23863  cnpflfi  23943  txflf  23950  fclscf  23969  flimfnfcls  23972  alexsubb  23990  alexsubALTlem2  23992  alexsubALTlem4  23994  ptcmplem2  23997  ptcmplem3  23998  cnextcn  24011  qustgplem  24065  prdsmet  24314  blin2  24373  prdsbl  24435  nmolb  24661  tgqioo  24744  reconnlem2  24772  reconn  24773  lebnumlem3  24918  iscau4  25235  cmetcaulem  25244  iscmet3lem2  25248  bcthlem5  25284  minveclem3b  25384  pmltpc  25407  evthicc2  25417  ovolunlem2  25455  ovolicc2lem5  25478  mblsplit  25489  iundisj2  25506  volsup  25513  ioombl1lem4  25518  dyaddisj  25553  dyadmbllem  25556  i1faddlem  25650  itg10a  25667  itg1ge0a  25668  mbfi1flimlem  25679  mbfmullem  25682  itg2add  25716  rolle  25950  dvcvx  25981  itgsubst  26012  tdeglem4  26021  ply1domn  26085  fta1b  26133  plyadd  26178  plymul  26179  coeeu  26186  vieta1  26276  aalioulem6  26301  ulmcaulem  26359  ulmcau  26360  ulmbdd  26363  ulmcn  26364  amgm  26957  mumullem2  27146  ppiublem1  27169  dchrfi  27222  dchrptlem2  27232  dchrptlem3  27233  dchrsum2  27235  lgsdchr  27322  lgsquad2lem2  27352  2sqlem5  27389  2sqb  27399  pntlemp  27577  ostthlem2  27595  ostth  27606  nosupprefixmo  27668  noinfprefixmo  27669  noetasuplem4  27704  madebdaylemlrcut  27895  addsproplem2  27966  precsexlem11  28213  ltonold  28257  bdayfinbndlem1  28463  iscgrglt  28586  tgbtwnconn1  28647  colline  28721  lmimid  28866  axcontlem8  29044  axcontlem9  29045  eengtrkg  29059  numedglnl  29217  uhgr2edg  29281  uspgr2wlkeq  29719  wlkonl1iedg  29737  wlkdlem2  29755  pthdlem2  29841  clwlkclwwlklem2a4  30072  clwwisshclwwsn  30091  clwwlknon1sn  30175  frgr2wwlkeu  30402  frgrreg  30469  frgrregord013  30470  nvmul0or  30725  ubthlem3  30947  axhcompl-zf  31073  hvmul0or  31100  ocnel  31373  pjhthmo  31377  spanuni  31619  spansni  31632  hon0  31868  leopadd  32207  leoptr  32212  mdsymlem6  32483  sumdmdlem2  32494  cdjreui  32507  iundisj2f  32665  disjunsn  32669  iundisj2fi  32877  ballotlemimin  34663  bnj23  34874  bnj594  35068  bnj849  35081  setindregs  35286  cusgr3cyclex  35330  txsconn  35435  cvmsdisj  35464  cvmliftlem15  35492  cvmlift2lem10  35506  cvmlift3lem7  35519  fmla1  35581  satffunlem1lem2  35597  satffunlem2lem2  35600  mclsppslem  35777  dfon2lem3  35977  dfon2lem5  35979  dfon2lem6  35980  dfon2lem7  35981  dfon2lem8  35982  ifscgr  36238  cgr3tr4  36246  btwnconn1lem13  36293  seglecgr12  36305  elicc3  36511  neibastop1  36553  tailfb  36571  bj-sblem2  37044  bj-sngltag  37184  copsex2d  37344  mptsnunlem  37543  finxpreclem6  37601  wl-equsal1i  37749  lindsenlbs  37816  poimirlem26  37847  poimirlem27  37848  ismblfin  37862  itg2addnclem3  37874  ftc1anclem6  37899  fdc  37946  riscer  38189  intidl  38230  ispridlc  38271  disjlem14  39057  disjlem17  39058  prtlem14  39134  prtlem17  39136  lpssat  39273  lssatle  39275  lshpkrlem6  39375  cvrnbtwn  39531  atlatmstc  39579  atlatle  39580  atlrelat1  39581  2at0mat0  39785  trlator0  40431  cdleme0moN  40485  cdlemn11pre  41470  dihord2pre  41485  dihmeetlem20N  41586  dochkrshp4  41649  lcfl6  41760  expeqidd  42580  remullid  42689  diophin  43014  diophun  43015  inaex  44538  pm10.57  44612  modelaxreplem1  45219  fnchoice  45274  ellimcabssub0  45863  fourierdlem81  46431  fourierdlem93  46443  2reuimp0  47360  fzopredsuc  47569  2ffzoeq  47573  m1modmmod  47604  iccpartlt  47670  ichnreuop  47718  prmdvdsfmtnof1lem1  47830  lighneallem4  47856  odd2prm2  47964  even3prm2  47965  sbgoldbst  48024  nnsum4primesevenALTV  48047  stgrvtx0  48208  isubgr3stgrlem6  48217  grlimprclnbgrvtx  48245  pgnbgreunbgr  48371  ply1mulgsumlem1  48632  snlindsntor  48717  islininds2  48730  itschlc0xyqsol1  49012  2itscp  49027  opnneir  49152  iscnrm3lem2  49180