Theorem syl5bir 242

Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 21-Jun-1993.)

Hypotheses

Ref	Expression
syl5bir.1	⊢ (𝜓 ↔ 𝜑)
syl5bir.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
syl5bir	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem syl5bir

Step	Hyp	Ref	Expression
1		syl5bir.1	. . 3 ⊢ (𝜓 ↔ 𝜑)
2	1	biimpri 227	. 2 ⊢ (𝜑 → 𝜓)
3		syl5bir.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 34	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  3imtr3g  295  oplem1  1054  nic-ax  1676  19.30  1885  19.33b  1889  necon1bd  2962  spc2d  3542  pssdifn0  4300  ralnralall  4450  disjss3  5074  somo  5541  frminex  5570  sofld  6095  predtrss  6229  ordelord  6292  unizlim  6387  f0rn0  6668  funopfv  6830  mpteqb  6903  fvrnressn  7042  funfvima  7115  fpropnf1  7149  fliftfun  7192  weniso  7234  tfinds  7715  tfindsg  7716  tfindes  7718  tfinds2  7719  findsg  7755  frxp  7976  suppssr  8021  rdgsucmptnf  8269  frsucmptn  8279  tz7.49  8285  om00  8415  oewordi  8431  iiner  8587  eroveu  8610  fsetexb  8661  undomOLD  8856  sucdom2OLD  8878  sdomdif  8921  pssnn  8960  sucdom2  8998  php3  9004  php3OLD  9016  unxpdomlem3  9038  fisseneq  9043  pssnnOLD  9049  ordunifi  9073  isfinite2  9081  fiint  9100  infssuni  9119  ixpfi2  9126  finsschain  9135  ordtypelem10  9295  wofib  9313  wemapsolem  9318  unxpwdom2  9356  inf3lem2  9396  cantnfp1lem3  9447  cantnfp1  9448  setind  9501  frr3g  9523  r1tr  9543  r1ordg  9545  rankelb  9591  rankxplim3  9648  updjudhf  9698  cardlim  9739  infxpenlem  9778  infxpenc2  9787  dfac5lem4  9891  dfac12k  9912  kmlem13  9927  sornom  10042  fin23lem25  10089  fin23lem21  10104  zorn2lem4  10264  iundom2g  10305  fpwwe2lem11  10406  fpwwe2lem12  10407  pwfseqlem4a  10426  eltsk2g  10516  inttsk  10539  tskord  10545  r1tskina  10547  grudomon  10582  arch  12239  zaddcl  12369  uzm1  12625  xrsupsslem  13050  xrinfmsslem  13051  fsequb  13704  fseqsupubi  13707  ssnn0fi  13714  seqf1o  13773  sq01  13949  ccatalpha  14307  swrdnd0  14379  repsdf2  14500  cshw1  14544  wrdl3s3  14686  rexanre  15067  rexuzre  15073  cau3lem  15075  o1co  15304  rlimcn3  15308  o1of2  15331  lo1add  15345  lo1mul  15346  climcau  15391  climbdd  15392  caucvgb  15400  summo  15438  isumltss  15569  mertenslem2  15606  prodmolem2  15654  prodmo  15655  dvdsaddre2b  16025  bitsfzolem  16150  bitsfzo  16151  bezoutlem4  16259  lcmfeq0b  16344  lcmfunsnlem2  16354  divgcdcoprmex  16380  prmind2  16399  2mulprm  16407  isprm5  16421  prm23ge5  16525  pcqmul  16563  pcadd  16599  prmreclem2  16627  prmreclem5  16630  mul4sq  16664  vdwmc2  16689  ramcl  16739  prmgaplem7  16767  prmlem1a  16817  setsstruct2  16884  divsfval  17267  iscatd2  17399  catpropd  17427  wunfunc  17623  wunfuncOLD  17624  cyccom  18831  gaorber  18923  psgneu  19123  lsmsubm  19267  pj1eu  19311  efgredlem  19362  qusabl  19475  cygablOLD  19501  cygctb  19502  lt6abl  19505  gsumval3eu  19514  dprdsubg  19636  ablfac1c  19683  pgpfac1  19692  dvdsrtr  19903  unitgrp  19918  drngmul0or  20021  lvecvs0or  20379  lspdisjb  20397  lspsolvlem  20413  lspprat  20424  lbsextlem2  20430  abvn0b  20582  domnchr  20745  znfld  20777  cygznlem3  20786  obselocv  20944  cpmatacl  21874  chfacfisf  22012  chfacfisfcpmat  22013  0ntr  22231  opnneiid  22286  restntr  22342  hausnei2  22513  nrmsep3  22515  cmpsub  22560  uncmp  22563  dfconn2  22579  cnconn  22582  1stcfb  22605  txuni2  22725  txbas  22727  ptbasin  22737  txcls  22764  txbasval  22766  txlly  22796  txnlly  22797  pthaus  22798  txlm  22808  tx1stc  22810  xkohaus  22813  isufil2  23068  ufileu  23079  cnpflfi  23159  txflf  23166  fclscf  23185  flimfnfcls  23188  alexsubb  23206  alexsubALTlem2  23208  alexsubALTlem4  23210  ptcmplem2  23213  ptcmplem3  23214  cnextcn  23227  qustgplem  23281  prdsmet  23532  blin2  23591  prdsbl  23656  nmolb  23890  tgqioo  23972  reconnlem2  23999  reconn  24000  lebnumlem3  24135  iscau4  24452  cmetcaulem  24461  iscmet3lem2  24465  bcthlem5  24501  minveclem3b  24601  pmltpc  24623  evthicc2  24633  ovolunlem2  24671  ovolicc2lem5  24694  mblsplit  24705  iundisj2  24722  volsup  24729  ioombl1lem4  24734  dyaddisj  24769  dyadmbllem  24772  i1faddlem  24866  itg10a  24884  itg1ge0a  24885  mbfi1flimlem  24896  mbfmullem  24899  itg2add  24933  rolle  25163  dvcvx  25193  itgsubst  25222  tdeglem4  25233  tdeglem4OLD  25234  ply1domn  25297  fta1b  25343  plyadd  25387  plymul  25388  coeeu  25395  vieta1  25481  aalioulem6  25506  ulmcaulem  25562  ulmcau  25563  ulmbdd  25566  ulmcn  25567  amgm  26149  mumullem2  26338  ppiublem1  26359  dchrfi  26412  dchrptlem2  26422  dchrptlem3  26423  dchrsum2  26425  lgsdchr  26512  lgsquad2lem2  26542  2sqlem5  26579  2sqb  26589  pntlemp  26767  ostthlem2  26785  ostth  26796  iscgrglt  26884  tgbtwnconn1  26945  colline  27019  lmimid  27164  axcontlem8  27348  axcontlem9  27349  eengtrkg  27363  numedglnl  27523  uhgr2edg  27584  uspgr2wlkeq  28022  wlkonl1iedg  28042  wlkdlem2  28060  pthdlem2  28145  clwlkclwwlklem2a4  28370  clwwisshclwwsn  28389  clwwlknon1sn  28473  frgr2wwlkeu  28700  frgrreg  28767  frgrregord013  28768  nvmul0or  29021  ubthlem3  29243  axhcompl-zf  29369  hvmul0or  29396  ocnel  29669  pjhthmo  29673  spanuni  29915  spansni  29928  hon0  30164  leopadd  30503  leoptr  30508  mdsymlem6  30779  sumdmdlem2  30790  cdjreui  30803  iundisj2f  30938  disjunsn  30942  iundisj2fi  31127  prmdvdsbc  31139  ballotlemimin  32481  bnj23  32706  bnj594  32901  bnj849  32914  cusgr3cyclex  33107  txsconn  33212  cvmsdisj  33241  cvmliftlem15  33269  cvmlift2lem10  33283  cvmlift3lem7  33296  fmla1  33358  satffunlem1lem2  33374  satffunlem2lem2  33377  mclsppslem  33554  dfon2lem3  33770  dfon2lem5  33772  dfon2lem6  33773  dfon2lem7  33774  dfon2lem8  33775  poxp2  33799  poxp3  33805  soseq  33812  nosupprefixmo  33912  noinfprefixmo  33913  noetasuplem4  33948  madebdaylemlrcut  34088  ifscgr  34355  cgr3tr4  34363  btwnconn1lem13  34410  seglecgr12  34422  elicc3  34515  neibastop1  34557  tailfb  34575  bj-sblem2  35036  bj-sngltag  35182  copsex2d  35319  mptsnunlem  35518  finxpreclem6  35576  wl-equsal1i  35711  lindsenlbs  35781  poimirlem26  35812  poimirlem27  35813  ismblfin  35827  itg2addnclem3  35839  ftc1anclem6  35864  fdc  35912  riscer  36155  intidl  36196  ispridlc  36237  prtlem14  36895  prtlem17  36897  lpssat  37034  lssatle  37036  lshpkrlem6  37136  cvrnbtwn  37292  atlatmstc  37340  atlatle  37341  atlrelat1  37342  2at0mat0  37546  trlator0  38192  cdleme0moN  38246  cdlemn11pre  39231  dihord2pre  39246  dihmeetlem20N  39347  dochkrshp4  39410  lcfl6  39521  remulid2  40422  diophin  40601  diophun  40602  inaex  41922  pm10.57  41996  fnchoice  42579  ellimcabssub0  43165  fourierdlem81  43735  fourierdlem93  43747  2reuimp0  44617  fzopredsuc  44826  2ffzoeq  44831  iccpartlt  44887  ichnreuop  44935  prmdvdsfmtnof1lem1  45047  lighneallem4  45073  odd2prm2  45181  even3prm2  45182  sbgoldbst  45241  nnsum4primesevenALTV  45264  nzerooringczr  45641  ply1mulgsumlem1  45738  snlindsntor  45823  islininds2  45836  m1modmmod  45878  itschlc0xyqsol1  46123  2itscp  46138  opnneir  46211  iscnrm3lem2  46239