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  2950  rexlimdvvva  3199  spc2d  3581  pssdifn0  4343  ralnralall  4490  disjss3  5118  somo  5600  frminex  5633  sofld  6176  predtrss  6311  ordelord  6374  unizlim  6476  f0rn0  6762  funopfv  6927  mpteqb  7004  fvrnressn  7150  funfvima  7221  fpropnf1  7259  fliftfun  7304  weniso  7346  tfinds  7853  tfindsg  7854  tfindes  7856  tfinds2  7857  findsg  7891  resf1ext2b  7929  frxp  8123  poxp2  8140  soseq  8156  suppssr  8192  rdgsucmptnf  8441  frsucmptn  8451  tz7.49  8457  om00  8585  oewordi  8601  iiner  8801  eroveu  8824  fsetexb  8876  undomOLD  9072  sucdom2OLD  9094  sdomdif  9137  pssnn  9180  sucdom2  9215  php3  9221  php3OLD  9231  unxpdomlem3  9258  fisseneq  9263  ordunifi  9296  isfinite2  9304  fiint  9336  fiintOLD  9337  infssuni  9356  ixpfi2  9360  finsschain  9369  ordtypelem10  9539  wofib  9557  wemapsolem  9562  unxpwdom2  9600  inf3lem2  9641  cantnfp1lem3  9692  cantnfp1  9693  setind  9746  frr3g  9768  r1tr  9788  r1ordg  9790  rankelb  9836  rankxplim3  9893  updjudhf  9943  cardlim  9984  infxpenlem  10025  infxpenc2  10034  dfac5lem4  10138  dfac5lem4OLD  10140  dfac12k  10160  kmlem13  10175  sornom  10289  fin23lem25  10336  fin23lem21  10351  zorn2lem4  10511  iundom2g  10552  fpwwe2lem11  10653  fpwwe2lem12  10654  pwfseqlem4a  10673  eltsk2g  10763  inttsk  10786  tskord  10792  r1tskina  10794  grudomon  10829  arch  12496  zaddcl  12630  uzm1  12888  xrsupsslem  13321  xrinfmsslem  13322  fsequb  13991  fseqsupubi  13994  ssnn0fi  14001  seqf1o  14059  sq01  14241  ccatalpha  14609  swrdnd0  14673  repsdf2  14794  cshw1  14838  wrdl3s3  14979  rexanre  15363  rexuzre  15369  cau3lem  15371  o1co  15600  rlimcn3  15604  o1of2  15627  lo1add  15641  lo1mul  15642  climcau  15685  climbdd  15686  caucvgb  15694  summo  15731  isumltss  15862  mertenslem2  15899  prodmolem2  15949  prodmo  15950  dvdsaddre2b  16324  bitsfzolem  16451  bitsfzo  16452  bezoutlem4  16559  lcmfeq0b  16647  lcmfunsnlem2  16657  divgcdcoprmex  16683  prmind2  16702  2mulprm  16710  isprm5  16724  prmdvdsbc  16743  prm23ge5  16833  pcqmul  16871  pcadd  16907  prmreclem2  16935  prmreclem5  16938  mul4sq  16972  vdwmc2  16997  ramcl  17047  prmgaplem7  17075  prmlem1a  17124  setsstruct2  17191  divsfval  17559  iscatd2  17691  catpropd  17719  wunfunc  17912  cyccom  19184  gaorber  19289  psgneu  19485  lsmsubm  19632  pj1eu  19675  efgredlem  19726  qusabl  19844  cygctb  19871  lt6abl  19874  gsumval3eu  19883  dprdsubg  20005  ablfac1c  20052  pgpfac1  20061  dvdsrtr  20326  unitgrp  20341  drngmul0orOLD  20719  abvn0b  20794  lvecvs0or  21067  lspdisjb  21085  lspsolvlem  21101  lspprat  21112  lbsextlem2  21118  nzerooringczr  21439  domnchr  21491  znfld  21519  cygznlem3  21528  obselocv  21686  cpmatacl  22652  chfacfisf  22790  chfacfisfcpmat  22791  0ntr  23007  opnneiid  23062  restntr  23118  hausnei2  23289  nrmsep3  23291  cmpsub  23336  uncmp  23339  dfconn2  23355  cnconn  23358  1stcfb  23381  txuni2  23501  txbas  23503  ptbasin  23513  txcls  23540  txbasval  23542  txlly  23572  txnlly  23573  pthaus  23574  txlm  23584  tx1stc  23586  xkohaus  23589  isufil2  23844  ufileu  23855  cnpflfi  23935  txflf  23942  fclscf  23961  flimfnfcls  23964  alexsubb  23982  alexsubALTlem2  23984  alexsubALTlem4  23986  ptcmplem2  23989  ptcmplem3  23990  cnextcn  24003  qustgplem  24057  prdsmet  24307  blin2  24366  prdsbl  24428  nmolb  24654  tgqioo  24737  reconnlem2  24765  reconn  24766  lebnumlem3  24911  iscau4  25229  cmetcaulem  25238  iscmet3lem2  25242  bcthlem5  25278  minveclem3b  25378  pmltpc  25401  evthicc2  25411  ovolunlem2  25449  ovolicc2lem5  25472  mblsplit  25483  iundisj2  25500  volsup  25507  ioombl1lem4  25512  dyaddisj  25547  dyadmbllem  25550  i1faddlem  25644  itg10a  25661  itg1ge0a  25662  mbfi1flimlem  25673  mbfmullem  25676  itg2add  25710  rolle  25944  dvcvx  25975  itgsubst  26006  tdeglem4  26015  ply1domn  26079  fta1b  26127  plyadd  26172  plymul  26173  coeeu  26180  vieta1  26270  aalioulem6  26295  ulmcaulem  26353  ulmcau  26354  ulmbdd  26357  ulmcn  26358  amgm  26951  mumullem2  27140  ppiublem1  27163  dchrfi  27216  dchrptlem2  27226  dchrptlem3  27227  dchrsum2  27229  lgsdchr  27316  lgsquad2lem2  27346  2sqlem5  27383  2sqb  27393  pntlemp  27571  ostthlem2  27589  ostth  27600  nosupprefixmo  27662  noinfprefixmo  27663  noetasuplem4  27698  madebdaylemlrcut  27854  addsproplem2  27920  precsexlem11  28158  sltonold  28200  iscgrglt  28439  tgbtwnconn1  28500  colline  28574  lmimid  28719  axcontlem8  28896  axcontlem9  28897  eengtrkg  28911  numedglnl  29069  uhgr2edg  29133  uspgr2wlkeq  29572  wlkonl1iedg  29591  wlkdlem2  29609  pthdlem2  29696  clwlkclwwlklem2a4  29924  clwwisshclwwsn  29943  clwwlknon1sn  30027  frgr2wwlkeu  30254  frgrreg  30321  frgrregord013  30322  nvmul0or  30577  ubthlem3  30799  axhcompl-zf  30925  hvmul0or  30952  ocnel  31225  pjhthmo  31229  spanuni  31471  spansni  31484  hon0  31720  leopadd  32059  leoptr  32064  mdsymlem6  32335  sumdmdlem2  32346  cdjreui  32359  iundisj2f  32517  disjunsn  32521  iundisj2fi  32720  ballotlemimin  34484  bnj23  34695  bnj594  34889  bnj849  34902  cusgr3cyclex  35104  txsconn  35209  cvmsdisj  35238  cvmliftlem15  35266  cvmlift2lem10  35280  cvmlift3lem7  35293  fmla1  35355  satffunlem1lem2  35371  satffunlem2lem2  35374  mclsppslem  35551  dfon2lem3  35749  dfon2lem5  35751  dfon2lem6  35752  dfon2lem7  35753  dfon2lem8  35754  ifscgr  36008  cgr3tr4  36016  btwnconn1lem13  36063  seglecgr12  36075  elicc3  36281  neibastop1  36323  tailfb  36341  bj-sblem2  36807  bj-sngltag  36947  copsex2d  37103  mptsnunlem  37302  finxpreclem6  37360  wl-equsal1i  37508  lindsenlbs  37585  poimirlem26  37616  poimirlem27  37617  ismblfin  37631  itg2addnclem3  37643  ftc1anclem6  37668  fdc  37715  riscer  37958  intidl  37999  ispridlc  38040  disjlem14  38762  disjlem17  38763  prtlem14  38838  prtlem17  38840  lpssat  38977  lssatle  38979  lshpkrlem6  39079  cvrnbtwn  39235  atlatmstc  39283  atlatle  39284  atlrelat1  39285  2at0mat0  39490  trlator0  40136  cdleme0moN  40190  cdlemn11pre  41175  dihord2pre  41190  dihmeetlem20N  41291  dochkrshp4  41354  lcfl6  41465  expeqidd  42321  remullid  42423  diophin  42742  diophun  42743  inaex  44269  pm10.57  44343  modelaxreplem1  44951  fnchoice  45001  ellimcabssub0  45594  fourierdlem81  46164  fourierdlem93  46176  2reuimp0  47091  fzopredsuc  47300  2ffzoeq  47304  iccpartlt  47386  ichnreuop  47434  prmdvdsfmtnof1lem1  47546  lighneallem4  47572  odd2prm2  47680  even3prm2  47681  sbgoldbst  47740  nnsum4primesevenALTV  47763  stgrvtx0  47922  isubgr3stgrlem6  47931  ply1mulgsumlem1  48310  snlindsntor  48395  islininds2  48408  m1modmmod  48449  itschlc0xyqsol1  48694  2itscp  48709  opnneir  48829  iscnrm3lem2  48857