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  1706  19.30  1914  19.33b  1918  sbrimvw  2128  necon1bd  2974  rexlimdvvva  3221  spc2d  3557  pssdifn0  4316  ralnralall  4469  disjss3  5102  somo  5598  frminex  5630  sofld  6179  predtrss  6325  ordelord  6384  unizlim  6487  f0rn0  6767  funopfv  6934  mpteqb  7013  fvrnressn  7165  funfvima  7236  fpropnf1  7271  fliftfun  7320  weniso  7364  tfinds  7871  tfindsg  7872  tfindes  7874  tfinds2  7875  findsg  7909  resf1ext2b  7947  frxp  8138  poxp2  8160  soseq  8176  suppssr  8212  rdgsucmptnf  8437  frsucmptn  8447  tz7.49  8455  om00  8583  oewordi  8600  iiner  8810  eroveu  8833  fsetexb  8886  sdomdif  9144  pssnn  9184  sucdom2  9218  php3  9224  unxpdomlem3  9249  fisseneq  9254  ordunifi  9281  isfinite2  9290  fiint  9318  infssuni  9335  ixpfi2  9339  finsschain  9348  ordtypelem10  9521  wofib  9539  wemapsolem  9544  unxpwdom2  9582  inf3lem2  9630  cantnfp1lem3  9681  cantnfp1  9682  setind  9748  frr3g  9760  r1tr  9783  r1ordg  9785  rankelb  9833  rankxplim3  9898  updjudhf  10012  cardlim  10053  infxpenlem  10092  infxpenc2  10101  dfac5lem4  10205  dfac12k  10226  kmlem13  10241  sornom  10355  fin23lem25  10402  fin23lem21  10417  zorn2lem4  10577  iundom2g  10624  fpwwe2lem11  10726  fpwwe2lem12  10727  pwfseqlem4a  10746  eltsk2g  10836  inttsk  10859  tskord  10865  r1tskina  10867  grudomon  10902  arch  12603  zaddcl  12736  uzm1  12999  xrsupsslem  13437  xrinfmsslem  13438  fsequb  14118  fseqsupubi  14121  ssnn0fi  14128  seqf1o  14186  sq01  14369  ccatalpha  14740  swrdnd0  14807  repsdf2  14929  cshw1  14973  wrdl3s3  15115  rexanre  15514  rexuzre  15520  cau3lem  15522  o1co  15753  rlimcn3  15757  o1of2  15780  lo1add  15794  lo1mul  15795  climcau  15838  climbdd  15839  caucvgb  15847  summo  15883  isumltss  16017  mertenslem2  16054  prodmolem2  16102  prodmo  16103  dvdsaddre2b  16477  bitsfzolem  16604  bitsfzo  16605  bezoutlem4  16715  lcmfeq0b  16805  lcmfunsnlem2  16815  divgcdcoprmex  16841  prmind2  16860  2mulprm  16868  isprm5  16883  prmdvdsbc  16902  prm23ge5  16993  pcqmul  17031  pcadd  17067  prmreclem2  17095  prmreclem5  17098  mul4sq  17132  vdwmc2  17157  ramcl  17207  prmgaplem7  17235  prmlem1a  17284  setsstruct2  17352  divsfval  17719  iscatd2  17855  catpropd  17883  wunfunc  18076  cyccom  19418  gaorber  19522  psgneu  19720  lsmsubm  19867  pj1eu  19910  efgredlem  19961  qusabl  20079  cygctb  20106  lt6abl  20109  gsumval3eu  20118  dprdsubg  20240  ablfac1c  20287  pgpfac1  20296  dvdsrtr  20598  unitgrp  20613  abvn0b  21093  lvecvs0or  21386  lspdisjb  21404  lspsolvlem  21420  lspprat  21431  lbsextlem2  21437  nzerooringczr  21786  domnchr  21838  znfld  21866  cygznlem3  21875  obselocv  22034  lindsenlbs  22157  cpmatacl  23034  chfacfisf  23172  chfacfisfcpmat  23173  0ntr  23389  opnneiid  23444  restntr  23500  hausnei2  23671  nrmsep3  23673  cmpsub  23718  uncmp  23721  dfconn2  23737  cnconn  23740  1stcfb  23763  txuni2  23884  txbas  23886  ptbasin  23896  txcls  23923  txbasval  23925  txlly  23955  txnlly  23956  pthaus  23957  txlm  23967  tx1stc  23969  xkohaus  23972  isufil2  24227  ufileu  24238  cnpflfi  24318  txflf  24325  fclscf  24344  flimfnfcls  24347  alexsubb  24365  alexsubALTlem2  24367  alexsubALTlem4  24369  ptcmplem2  24372  ptcmplem3  24373  cnextcn  24386  qustgplem  24440  prdsmet  24689  blin2  24748  prdsbl  24810  nmolb  25036  tgqioo  25119  reconnlem2  25147  reconn  25148  lebnumlem3  25284  iscau4  25600  cmetcaulem  25609  iscmet3lem2  25613  bcthlem5  25649  minveclem3b  25749  pmltpc  25771  evthicc2  25781  ovolunlem2  25819  ovolicc2lem5  25842  mblsplit  25853  iundisj2  25870  volsup  25877  ioombl1lem4  25882  dyaddisj  25917  dyadmbllem  25920  i1faddlem  26014  itg10a  26031  itg1ge0a  26032  mbfi1flimlem  26043  mbfmullem  26046  itg2add  26080  rolle  26310  dvcvx  26340  itgsubst  26369  tdeglem4  26378  ply1domn  26442  fta1b  26490  plyadd  26536  plymul  26537  coeeu  26544  vieta1  26635  aalioulem6  26664  ulmcaulem  26721  ulmcau  26722  ulmbdd  26725  ulmcn  26726  amgm  27318  mumullem2  27507  ppiublem1  27529  dchrfi  27582  dchrptlem2  27592  dchrptlem3  27593  dchrsum2  27595  lgsdchr  27682  lgsquad2lem2  27712  2sqlem5  27749  2sqb  27759  pntlemp  27937  ostthlem2  27955  ostth  27966  nosupprefixmo  28057  noinfprefixmo  28058  noetasuplem4  28093  madebdaylemlrcut  28285  addsproplem2  28356  precsexlem11  28603  ltonold  28647  bdayfinbndlem1  28853  iscgrglt  28977  tgbtwnconn1  29038  colline  29118  lmimid  29299  axcontlem8  29549  axcontlem9  29550  eengtrkg  29564  numedglnl  29722  uhgr2edg  29789  uspgr2wlkeq  30226  wlkonl1iedg  30244  wlkdlem2  30262  pthdlem2  30354  clwlkclwwlklem2a4  30588  clwwisshclwwsn  30607  clwwlknon1sn  30691  frgr2wwlkeu  30928  frgrreg  30995  frgrregord013  30996  nvmul0or  31252  ubthlem3  31474  axhcompl-zf  31600  hvmul0or  31627  ocnel  31900  pjhthmo  31904  spanuni  32146  spansni  32159  hon0  32395  leopadd  32734  leoptr  32739  mdsymlem6  33010  sumdmdlem2  33021  cdjreui  33034  iundisj2f  33184  disjunsn  33188  iundisj2fi  33389  ballotlemimin  35138  bnj23  35349  bnj594  35542  bnj849  35555  setindregs  35798  karddom  35829  kardsdom  35830  cusgr3cyclex  35911  txsconn  36006  cvmsdisj  36035  cvmliftlem15  36063  cvmlift2lem10  36077  cvmlift3lem7  36090  fmla1  36152  satffunlem1lem2  36168  satffunlem2lem2  36171  mclsppslem  36348  dfon2lem3  36547  dfon2lem5  36549  dfon2lem6  36550  dfon2lem7  36551  dfon2lem8  36552  ifscgr  36809  cgr3tr4  36817  btwnconn1lem13  36864  seglecgr12  36876  elicc3  37105  neibastop1  37147  tailfb  37165  bj-sblem2  37755  bj-sngltag  37896  copsex2d  38060  mptsnunlem  38261  finxpreclem6  38319  wl-equsal1i  38476  poimirlem26  38564  poimirlem27  38565  ismblfin  38579  itg2addnclem3  38591  ftc1anclem6  38616  fdc  38679  riscer  38922  intidl  38963  ispridlc  39004  disjlem14  39833  disjlem17  39834  prtlem14  39931  prtlem17  39933  lpssat  40070  lssatle  40072  lshpkrlem6  40172  cvrnbtwn  40328  atlatmstc  40376  atlatle  40377  atlrelat1  40378  2at0mat0  40582  trlator0  41228  cdleme0moN  41282  cdlemn11pre  42267  dihord2pre  42282  dihmeetlem20N  42383  dochkrshp4  42446  lcfl6  42557  expeqidd  43382  remullid  43485  diophin  43782  diophun  43783  inaex  45280  pm10.57  45354  modelaxreplem1  45967  fnchoice  46045  ellimcabssub0  46628  fourierdlem81  47196  fourierdlem93  47208  2reuimp0  48183  fzopredsuc  48393  2ffzoeq  48397  m1modmmod  48433  iccpartlt  48505  ichnreuop  48553  prmdvdsfmtnof1lem1  48668  lighneallem4  48694  odd2prm2  48815  even3prm2  48816  sbgoldbst  48875  nnsum4primesevenALTV  48898  stgrvtx0  49059  isubgr3stgrlem6  49068  grlimprclnbgrvtx  49096  pgnbgreunbgr  49222  ply1mulgsumlem1  49497  snlindsntor  49582  islininds2  49595  itschlc0xyqsol1  49877  2itscp  49892  opnneir  50014  iscnrm3lem2  50042