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  2973  rexlimdvvva  3220  spc2d  3556  pssdifn0  4316  ralnralall  4469  disjss3  5102  somo  5602  frminex  5634  sofld  6180  predtrss  6320  ordelord  6379  unizlim  6482  f0rn0  6761  funopfv  6928  mpteqb  7007  fvrnressn  7159  funfvima  7230  fpropnf1  7265  fliftfun  7314  weniso  7358  tfinds  7857  tfindsg  7858  tfindes  7860  tfinds2  7861  findsg  7895  resf1ext2b  7933  frxp  8125  poxp2  8142  soseq  8158  suppssr  8194  rdgsucmptnf  8419  frsucmptn  8429  tz7.49  8437  om00  8565  oewordi  8582  iiner  8792  eroveu  8815  fsetexb  8868  sdomdif  9126  pssnn  9166  sucdom2  9200  php3  9206  unxpdomlem3  9231  fisseneq  9236  ordunifi  9263  isfinite2  9271  fiint  9299  infssuni  9316  ixpfi2  9320  finsschain  9329  ordtypelem10  9502  wofib  9520  wemapsolem  9525  unxpwdom2  9563  inf3lem2  9611  cantnfp1lem3  9662  cantnfp1  9663  setind  9729  frr3g  9741  r1tr  9761  r1ordg  9763  rankelb  9809  rankxplim3  9866  updjudhf  9939  cardlim  9980  infxpenlem  10019  infxpenc2  10028  dfac5lem4  10132  dfac12k  10153  kmlem13  10168  sornom  10282  fin23lem25  10329  fin23lem21  10344  zorn2lem4  10504  iundom2g  10551  fpwwe2lem11  10653  fpwwe2lem12  10654  pwfseqlem4a  10673  eltsk2g  10763  inttsk  10786  tskord  10792  r1tskina  10794  grudomon  10829  arch  12528  zaddcl  12661  uzm1  12924  xrsupsslem  13362  xrinfmsslem  13363  fsequb  14042  fseqsupubi  14045  ssnn0fi  14052  seqf1o  14110  sq01  14292  ccatalpha  14663  swrdnd0  14730  repsdf2  14852  cshw1  14896  wrdl3s3  15038  rexanre  15437  rexuzre  15443  cau3lem  15445  o1co  15676  rlimcn3  15680  o1of2  15703  lo1add  15717  lo1mul  15718  climcau  15761  climbdd  15762  caucvgb  15770  summo  15806  isumltss  15940  mertenslem2  15977  prodmolem2  16025  prodmo  16026  dvdsaddre2b  16400  bitsfzolem  16527  bitsfzo  16528  bezoutlem4  16635  lcmfeq0b  16723  lcmfunsnlem2  16733  divgcdcoprmex  16759  prmind2  16778  2mulprm  16786  isprm5  16801  prmdvdsbc  16820  prm23ge5  16910  pcqmul  16948  pcadd  16984  prmreclem2  17012  prmreclem5  17015  mul4sq  17049  vdwmc2  17074  ramcl  17124  prmgaplem7  17152  prmlem1a  17201  setsstruct2  17269  divsfval  17636  iscatd2  17772  catpropd  17800  wunfunc  17993  cyccom  19334  gaorber  19438  psgneu  19636  lsmsubm  19783  pj1eu  19826  efgredlem  19877  qusabl  19995  cygctb  20022  lt6abl  20025  gsumval3eu  20034  dprdsubg  20156  ablfac1c  20203  pgpfac1  20212  dvdsrtr  20512  unitgrp  20527  abvn0b  21005  lvecvs0or  21298  lspdisjb  21316  lspsolvlem  21332  lspprat  21343  lbsextlem2  21349  nzerooringczr  21696  domnchr  21748  znfld  21776  cygznlem3  21785  obselocv  21944  lindsenlbs  22067  cpmatacl  22944  chfacfisf  23082  chfacfisfcpmat  23083  0ntr  23299  opnneiid  23354  restntr  23410  hausnei2  23581  nrmsep3  23583  cmpsub  23628  uncmp  23631  dfconn2  23647  cnconn  23650  1stcfb  23673  txuni2  23794  txbas  23796  ptbasin  23806  txcls  23833  txbasval  23835  txlly  23865  txnlly  23866  pthaus  23867  txlm  23877  tx1stc  23879  xkohaus  23882  isufil2  24137  ufileu  24148  cnpflfi  24228  txflf  24235  fclscf  24254  flimfnfcls  24257  alexsubb  24275  alexsubALTlem2  24277  alexsubALTlem4  24279  ptcmplem2  24282  ptcmplem3  24283  cnextcn  24296  qustgplem  24350  prdsmet  24599  blin2  24658  prdsbl  24720  nmolb  24946  tgqioo  25029  reconnlem2  25057  reconn  25058  lebnumlem3  25194  iscau4  25510  cmetcaulem  25519  iscmet3lem2  25523  bcthlem5  25559  minveclem3b  25659  pmltpc  25681  evthicc2  25691  ovolunlem2  25729  ovolicc2lem5  25752  mblsplit  25763  iundisj2  25780  volsup  25787  ioombl1lem4  25792  dyaddisj  25827  dyadmbllem  25830  i1faddlem  25924  itg10a  25941  itg1ge0a  25942  mbfi1flimlem  25953  mbfmullem  25956  itg2add  25990  rolle  26220  dvcvx  26250  itgsubst  26279  tdeglem4  26288  ply1domn  26352  fta1b  26400  plyadd  26446  plymul  26447  coeeu  26454  vieta1  26547  aalioulem6  26576  ulmcaulem  26633  ulmcau  26634  ulmbdd  26637  ulmcn  26638  amgm  27230  mumullem2  27419  ppiublem1  27441  dchrfi  27494  dchrptlem2  27504  dchrptlem3  27505  dchrsum2  27507  lgsdchr  27594  lgsquad2lem2  27624  2sqlem5  27661  2sqb  27671  pntlemp  27849  ostthlem2  27867  ostth  27878  nosupprefixmo  27939  noinfprefixmo  27940  noetasuplem4  27975  madebdaylemlrcut  28167  addsproplem2  28238  precsexlem11  28485  ltonold  28529  bdayfinbndlem1  28735  iscgrglt  28859  tgbtwnconn1  28920  colline  29000  lmimid  29181  axcontlem8  29431  axcontlem9  29432  eengtrkg  29446  numedglnl  29604  uhgr2edg  29671  uspgr2wlkeq  30108  wlkonl1iedg  30126  wlkdlem2  30144  pthdlem2  30236  clwlkclwwlklem2a4  30470  clwwisshclwwsn  30489  clwwlknon1sn  30573  frgr2wwlkeu  30810  frgrreg  30877  frgrregord013  30878  nvmul0or  31134  ubthlem3  31356  axhcompl-zf  31482  hvmul0or  31509  ocnel  31782  pjhthmo  31786  spanuni  32028  spansni  32041  hon0  32277  leopadd  32616  leoptr  32621  mdsymlem6  32892  sumdmdlem2  32903  cdjreui  32916  iundisj2f  33066  disjunsn  33070  iundisj2fi  33271  ballotlemimin  35020  bnj23  35231  bnj594  35424  bnj849  35437  setindregs  35659  karddom  35690  kardsdom  35691  cusgr3cyclex  35728  txsconn  35823  cvmsdisj  35852  cvmliftlem15  35880  cvmlift2lem10  35894  cvmlift3lem7  35907  fmla1  35969  satffunlem1lem2  35985  satffunlem2lem2  35988  mclsppslem  36165  dfon2lem3  36365  dfon2lem5  36367  dfon2lem6  36368  dfon2lem7  36369  dfon2lem8  36370  ifscgr  36627  cgr3tr4  36635  btwnconn1lem13  36682  seglecgr12  36694  elicc3  36939  neibastop1  36981  tailfb  36999  bj-sblem2  37589  bj-sngltag  37730  copsex2d  37894  mptsnunlem  38095  finxpreclem6  38153  wl-equsal1i  38310  poimirlem26  38398  poimirlem27  38399  ismblfin  38413  itg2addnclem3  38425  ftc1anclem6  38450  fdc  38498  riscer  38741  intidl  38782  ispridlc  38823  disjlem14  39652  disjlem17  39653  prtlem14  39750  prtlem17  39752  lpssat  39889  lssatle  39891  lshpkrlem6  39991  cvrnbtwn  40147  atlatmstc  40195  atlatle  40196  atlrelat1  40197  2at0mat0  40401  trlator0  41047  cdleme0moN  41101  cdlemn11pre  42086  dihord2pre  42101  dihmeetlem20N  42202  dochkrshp4  42265  lcfl6  42376  expeqidd  43203  remullid  43312  diophin  43620  diophun  43621  inaex  45124  pm10.57  45198  modelaxreplem1  45804  fnchoice  45866  ellimcabssub0  46450  fourierdlem81  47018  fourierdlem93  47030  2reuimp0  48005  fzopredsuc  48215  2ffzoeq  48219  m1modmmod  48255  iccpartlt  48327  ichnreuop  48375  prmdvdsfmtnof1lem1  48490  lighneallem4  48516  odd2prm2  48637  even3prm2  48638  sbgoldbst  48697  nnsum4primesevenALTV  48720  stgrvtx0  48881  isubgr3stgrlem6  48890  grlimprclnbgrvtx  48918  pgnbgreunbgr  49044  ply1mulgsumlem1  49319  snlindsntor  49404  islininds2  49417  itschlc0xyqsol1  49699  2itscp  49714  opnneir  49836  iscnrm3lem2  49864