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  2978  rexlimdvvva  3225  spc2d  3563  pssdifn0  4323  ralnralall  4476  disjss3  5110  somo  5610  frminex  5642  sofld  6187  predtrss  6327  ordelord  6386  unizlim  6489  f0rn0  6767  funopfv  6934  mpteqb  7013  fvrnressn  7164  funfvima  7235  fpropnf1  7270  fliftfun  7319  weniso  7363  tfinds  7862  tfindsg  7863  tfindes  7865  tfinds2  7866  findsg  7900  resf1ext2b  7938  frxp  8128  poxp2  8145  soseq  8161  suppssr  8197  rdgsucmptnf  8422  frsucmptn  8432  tz7.49  8438  om00  8566  oewordi  8583  iiner  8793  eroveu  8816  fsetexb  8867  sdomdif  9120  pssnn  9160  sucdom2  9194  php3  9200  unxpdomlem3  9225  fisseneq  9230  ordunifi  9257  isfinite2  9265  fiint  9293  infssuni  9310  ixpfi2  9314  finsschain  9323  ordtypelem10  9496  wofib  9514  wemapsolem  9519  unxpwdom2  9557  inf3lem2  9605  cantnfp1lem3  9656  cantnfp1  9657  setind  9723  frr3g  9735  r1tr  9755  r1ordg  9757  rankelb  9803  rankxplim3  9860  updjudhf  9933  cardlim  9974  infxpenlem  10013  infxpenc2  10022  dfac5lem4  10126  dfac12k  10147  kmlem13  10162  sornom  10276  fin23lem25  10323  fin23lem21  10338  zorn2lem4  10498  iundom2g  10541  fpwwe2lem11  10643  fpwwe2lem12  10644  pwfseqlem4a  10663  eltsk2g  10753  inttsk  10776  tskord  10782  r1tskina  10784  grudomon  10819  arch  12518  zaddcl  12651  uzm1  12914  xrsupsslem  13351  xrinfmsslem  13352  fsequb  14031  fseqsupubi  14034  ssnn0fi  14041  seqf1o  14099  sq01  14281  ccatalpha  14652  swrdnd0  14719  repsdf2  14841  cshw1  14885  wrdl3s3  15025  rexanre  15424  rexuzre  15430  cau3lem  15432  o1co  15663  rlimcn3  15667  o1of2  15690  lo1add  15704  lo1mul  15705  climcau  15748  climbdd  15749  caucvgb  15757  summo  15793  isumltss  15927  mertenslem2  15964  prodmolem2  16014  prodmo  16015  dvdsaddre2b  16389  bitsfzolem  16516  bitsfzo  16517  bezoutlem4  16624  lcmfeq0b  16712  lcmfunsnlem2  16722  divgcdcoprmex  16748  prmind2  16767  2mulprm  16775  isprm5  16790  prmdvdsbc  16809  prm23ge5  16899  pcqmul  16937  pcadd  16973  prmreclem2  17001  prmreclem5  17004  mul4sq  17038  vdwmc2  17063  ramcl  17113  prmgaplem7  17141  prmlem1a  17190  setsstruct2  17258  divsfval  17625  iscatd2  17761  catpropd  17789  wunfunc  17982  cyccom  19320  gaorber  19424  psgneu  19622  lsmsubm  19769  pj1eu  19812  efgredlem  19863  qusabl  19981  cygctb  20008  lt6abl  20011  gsumval3eu  20020  dprdsubg  20142  ablfac1c  20189  pgpfac1  20198  dvdsrtr  20498  unitgrp  20513  abvn0b  20991  lvecvs0or  21284  lspdisjb  21302  lspsolvlem  21318  lspprat  21329  lbsextlem2  21335  nzerooringczr  21682  domnchr  21734  znfld  21762  cygznlem3  21771  obselocv  21930  cpmatacl  22925  chfacfisf  23063  chfacfisfcpmat  23064  0ntr  23280  opnneiid  23335  restntr  23391  hausnei2  23562  nrmsep3  23564  cmpsub  23609  uncmp  23612  dfconn2  23628  cnconn  23631  1stcfb  23654  txuni2  23775  txbas  23777  ptbasin  23787  txcls  23814  txbasval  23816  txlly  23846  txnlly  23847  pthaus  23848  txlm  23858  tx1stc  23860  xkohaus  23863  isufil2  24118  ufileu  24129  cnpflfi  24209  txflf  24216  fclscf  24235  flimfnfcls  24238  alexsubb  24256  alexsubALTlem2  24258  alexsubALTlem4  24260  ptcmplem2  24263  ptcmplem3  24264  cnextcn  24277  qustgplem  24331  prdsmet  24580  blin2  24639  prdsbl  24701  nmolb  24927  tgqioo  25010  reconnlem2  25038  reconn  25039  lebnumlem3  25175  iscau4  25491  cmetcaulem  25500  iscmet3lem2  25504  bcthlem5  25540  minveclem3b  25640  pmltpc  25662  evthicc2  25672  ovolunlem2  25710  ovolicc2lem5  25733  mblsplit  25744  iundisj2  25761  volsup  25768  ioombl1lem4  25773  dyaddisj  25808  dyadmbllem  25811  i1faddlem  25905  itg10a  25922  itg1ge0a  25923  mbfi1flimlem  25934  mbfmullem  25937  itg2add  25971  rolle  26202  dvcvx  26232  itgsubst  26261  tdeglem4  26270  ply1domn  26334  fta1b  26382  plyadd  26427  plymul  26428  coeeu  26435  vieta1  26526  aalioulem6  26553  ulmcaulem  26610  ulmcau  26611  ulmbdd  26614  ulmcn  26615  amgm  27208  mumullem2  27397  ppiublem1  27419  dchrfi  27472  dchrptlem2  27482  dchrptlem3  27483  dchrsum2  27485  lgsdchr  27572  lgsquad2lem2  27602  2sqlem5  27639  2sqb  27649  pntlemp  27827  ostthlem2  27845  ostth  27856  nosupprefixmo  27917  noinfprefixmo  27918  noetasuplem4  27953  madebdaylemlrcut  28145  addsproplem2  28216  precsexlem11  28463  ltonold  28507  bdayfinbndlem1  28713  iscgrglt  28836  tgbtwnconn1  28897  colline  28976  lmimid  29156  axcontlem8  29378  axcontlem9  29379  eengtrkg  29393  numedglnl  29551  uhgr2edg  29618  uspgr2wlkeq  30055  wlkonl1iedg  30073  wlkdlem2  30091  pthdlem2  30183  clwlkclwwlklem2a4  30417  clwwisshclwwsn  30436  clwwlknon1sn  30520  frgr2wwlkeu  30751  frgrreg  30818  frgrregord013  30819  nvmul0or  31075  ubthlem3  31297  axhcompl-zf  31423  hvmul0or  31450  ocnel  31723  pjhthmo  31727  spanuni  31969  spansni  31982  hon0  32218  leopadd  32557  leoptr  32562  mdsymlem6  32833  sumdmdlem2  32844  cdjreui  32857  iundisj2f  33008  disjunsn  33012  iundisj2fi  33214  ballotlemimin  34963  bnj23  35174  bnj594  35367  bnj849  35380  setindregs  35602  karddom  35633  kardsdom  35634  cusgr3cyclex  35671  txsconn  35772  cvmsdisj  35801  cvmliftlem15  35829  cvmlift2lem10  35843  cvmlift3lem7  35856  fmla1  35918  satffunlem1lem2  35934  satffunlem2lem2  35937  mclsppslem  36114  dfon2lem3  36314  dfon2lem5  36316  dfon2lem6  36317  dfon2lem7  36318  dfon2lem8  36319  ifscgr  36575  cgr3tr4  36583  btwnconn1lem13  36630  seglecgr12  36642  elicc3  36887  neibastop1  36929  tailfb  36947  bj-sblem2  37537  bj-sngltag  37678  copsex2d  37842  mptsnunlem  38043  finxpreclem6  38101  wl-equsal1i  38258  lindsenlbs  38325  poimirlem26  38356  poimirlem27  38357  ismblfin  38371  itg2addnclem3  38383  ftc1anclem6  38408  fdc  38456  riscer  38699  intidl  38740  ispridlc  38781  disjlem14  39610  disjlem17  39611  prtlem14  39708  prtlem17  39710  lpssat  39847  lssatle  39849  lshpkrlem6  39949  cvrnbtwn  40105  atlatmstc  40153  atlatle  40154  atlrelat1  40155  2at0mat0  40359  trlator0  41005  cdleme0moN  41059  cdlemn11pre  42044  dihord2pre  42059  dihmeetlem20N  42160  dochkrshp4  42223  lcfl6  42334  expeqidd  43146  remullid  43255  diophin  43563  diophun  43564  inaex  45067  pm10.57  45141  modelaxreplem1  45747  fnchoice  45809  ellimcabssub0  46393  fourierdlem81  46961  fourierdlem93  46973  2reuimp0  47911  fzopredsuc  48121  2ffzoeq  48125  m1modmmod  48161  iccpartlt  48233  ichnreuop  48281  prmdvdsfmtnof1lem1  48396  lighneallem4  48422  odd2prm2  48543  even3prm2  48544  sbgoldbst  48603  nnsum4primesevenALTV  48626  stgrvtx0  48787  isubgr3stgrlem6  48796  grlimprclnbgrvtx  48824  pgnbgreunbgr  48950  ply1mulgsumlem1  49225  snlindsntor  49310  islininds2  49323  itschlc0xyqsol1  49605  2itscp  49620  opnneir  49744  iscnrm3lem2  49772