Theorem syl6ib 250

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

Hypotheses

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

Assertion

Ref	Expression
syl6ib	⊢ (𝜑 → (𝜓 → 𝜃))

Proof of Theorem syl6ib

Step	Hyp	Ref	Expression
1		syl6ib.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		syl6ib.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	2	biimpi 215	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 35	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  294  3orel2  1485  exlimd  2211  cbvexdw  2335  ax13lem2  2374  cbvexd  2406  axc14  2461  mo3  2557  2eu3  2648  2eu6  2651  necon2bd  2955  necon2d  2962  necon4d  2963  spcimgft  3547  spc3egv  3563  elabgt  3627  reupick  4283  prneimg  4817  dfiun2g  4995  invdisj  5094  trin  5239  exexneq  5396  pwssun  5533  wefrc  5632  eqbrrdva  5830  elreldm  5895  elinxp  5980  xp11  6132  ssrnres  6135  suc11  6429  opelf  6708  dffo4  7058  onmindif2  7747  dftpos3  8180  frrlem13  8234  swoer  8685  domtriord  9074  nneneq  9160  nneneqOLD  9172  unblem1  9246  supnub  9407  infnlb  9437  en3lplem2  9558  suc11reg  9564  inf3lem2  9574  trcl  9673  tz9.13  9736  acndom  9996  carduniima  10041  cardinfima  10042  dfac5lem5  10072  fin23lem26  10270  hsmexlem2  10372  axcc4  10384  axdc3lem2  10396  axdclem2  10465  entric  10502  alephval2  10517  cfpwsdom  10529  fpwwe2lem8  10583  ltapr  10990  supsrlem  11056  sup2  12120  nnunb  12418  nneo  12596  indstr  12850  mul2lt0bi  13030  ngtmnft  13095  qsqueeze  13130  qextlt  13132  qextle  13133  icoshft  13400  injresinj  13703  swrdccatin2  14629  rexuzre  15249  rexico  15250  summo  15613  rpnnen2lem12  16118  divalglem5  16290  ndvdssub  16302  isprm7  16595  prmdvdsncoprmbd  16613  pc2dvds  16762  infpn2  16796  vdwnnlem3  16880  mreiincl  17490  intopsn  18523  pmtrrn2  19256  psgnunilem4  19293  ablfac1eulem  19865  lbsextlem3  20680  xrsdsreclb  20881  znleval  20998  elcls3  22471  isclo2  22476  tgcn  22640  cnprest  22677  ordthaus  22772  hauscmplem  22794  comppfsc  22920  kgencn2  22945  prdstopn  23016  xkohaus  23041  qtoptop2  23087  tgqtop  23100  filufint  23308  fclsbas  23409  alexsubALTlem3  23437  alexsubALTlem4  23438  ptcmplem2  23441  cldsubg  23499  isucn2  23668  metequiv2  23903  bcthlem5  24729  vieta1  25709  aannenlem2  25726  ulmbdd  25794  angpined  26217  rlimcnp2  26353  amgm  26377  ftalem3  26461  bposlem6  26674  nofv  27042  sltres  27047  nogt01o  27081  nosupprefixmo  27085  noinfprefixmo  27086  noetasuplem4  27121  uhgrvd00  28545  pthdlem2lem  28778  frcond2  29274  lnon0  29803  ocnel  30303  h1dn0  30557  cnlnssadj  31085  cvnbtwn2  31292  cvnbtwn3  31293  cvnbtwn4  31294  dmdbr2  31308  dmdbr3  31310  dmdbr4  31311  superpos  31359  atcvati  31391  mdsymlem4  31411  sumdmdii  31420  cdj3lem1  31439  elicoelioo  31749  archiabl  32104  bnj1280  33721  cusgr3cyclex  33817  loop1cycl  33818  erdszelem9  33880  satfvsucsuc  34046  untangtr  34372  dfon2lem6  34449  dfon2lem7  34450  outsideofrflx  34788  trer  34864  elicc3  34865  nn0prpw  34871  bj-syl66ib  35094  bj-cbvexdv  35341  bj-sblem1  35384  bj-spcimdv  35438  bj-spcimdvv  35439  topdifinffinlem  35891  icorempo  35895  isbasisrelowllem1  35899  relowlpssretop  35908  difunieq  35918  fvineqsneq  35956  wl-mo3t  36104  poimirlem23  36174  poimirlem29  36180  poimirlem32  36183  poimir  36184  mblfinlem2  36189  sdclem1  36275  fdc  36277  incsequz  36280  rngosn3  36456  0rngo  36559  dmncan1  36608  disjdmqscossss  37338  bicomdd  37389  prtlem15  37410  lsatcvat  37585  lfl1  37605  hlrelat2  37939  cvrat  37958  linepsubN  38288  2llnma3r  38324  dihjatcclem4  39957  dochexmidlem1  39996  sn-sup2  40996  rngunsnply  41558  onsupuni  41621  tfsconcatrn  41735  mptrcllem  42007  frege124d  42155  frege77  42334  frege116  42373  or3or  42417  clsk1indlem3  42437  ssralv2  42935  truniALT  42945  onfrALTlem3  42948  onfrALTlem2  42950  onfrALTlem1  42952  ax6e2ndeq  42963  stoweidlem62  44423  atbiffatnnb  45267  2reu3  45462  2reuimp  45467  gbowge7  46075  gbege6  46077  copisnmnd  46223  line2ylem  46957  line2xlem  46959  setrec1lem4  47255