Theorem syl6ib 240

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 205	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 34	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  3imtr3g  283  exp4aOLD  632  mtord  690  19.23v  1889  exlimd  2074  exlimdOLD  2211  cbvexd  2266  ax13lem2  2284  axc14  2360  mo3  2495  2eu3  2543  2eu6  2546  exists2  2550  necon2bd  2798  necon2d  2805  necon4d  2806  spcimgft  3257  eqsbc3rOLD  3460  reupick  3870  prneimg  4328  invdisj  4571  trin  4691  pwssun  4944  wefrc  5032  eqbrrdva  5213  elreldm  5271  elres  5355  xp11  5488  ssrnres  5491  ordtri3OLD  5677  suc11  5748  opelf  5978  dffo4  6283  onmindif2  6904  dftpos3  7257  swoer  7659  mapsn  7785  domtriord  7991  nneneq  8028  unblem1  8097  supnub  8251  infnlb  8281  en3lplem2  8395  suc11reg  8399  inf3lem2  8409  trcl  8487  tz9.13  8537  acndom  8757  carduniima  8802  cardinfima  8803  dfac5lem5  8833  fin23lem26  9030  hsmexlem2  9132  axcc4  9144  axdc3lem2  9156  axdclem2  9225  entric  9258  alephval2  9273  cfpwsdom  9285  fpwwe2lem9  9339  ltapr  9746  supsrlem  9811  sup2  10858  nnunb  11165  nneo  11337  indstr  11632  mul2lt0bi  11812  ngtmnft  11872  qsqueeze  11906  qextlt  11908  qextle  11909  icoshft  12165  injresinj  12451  rexuzre  13940  rexico  13941  summo  14295  rpnnen2lem12  14793  divalglem5  14958  ndvdssub  14971  isprm7  15258  pc2dvds  15421  infpn2  15455  vdwnnlem3  15539  mreiincl  16079  intopsn  17076  pmtrrn2  17703  psgnunilem4  17740  ablfac1eulem  18294  lbsextlem3  18981  xrsdsreclb  19612  znleval  19722  elcls3  20697  isclo2  20702  tgcn  20866  cnprest  20903  ordthaus  20998  hauscmplem  21019  comppfsc  21145  kgencn2  21170  prdstopn  21241  xkohaus  21266  qtoptop2  21312  tgqtop  21325  filufint  21534  fclsbas  21635  alexsubALTlem3  21663  alexsubALTlem4  21664  ptcmplem2  21667  cldsubg  21724  isucn2  21893  metequiv2  22125  bcthlem5  22933  vieta1  23871  aannenlem2  23888  ulmbdd  23956  angpined  24357  rlimcnp2  24493  amgm  24517  ftalem3  24601  bposlem6  24814  upgredg  25811  cusgrares  26001  frgraun  26523  usgreg2spot  26594  lnon0  27037  ocnel  27541  h1dn0  27795  cnlnssadj  28323  cvnbtwn2  28530  cvnbtwn3  28531  cvnbtwn4  28532  dmdbr2  28546  dmdbr3  28548  dmdbr4  28549  superpos  28597  atcvati  28629  mdsymlem4  28649  sumdmdii  28658  cdj3lem1  28677  elicoelioo  28930  archiabl  29083  bnj1280  30342  erdszelem9  30435  untangtr  30845  3orel2  30847  dfon2lem6  30937  dfon2lem7  30938  nofv  31054  sltres  31061  nodenselem4  31083  nodenselem7  31086  outsideofrflx  31404  trer  31480  elicc3  31481  nn0prpw  31488  bj-cbvexdv  31923  bj-syl66ib  32023  bj-spcimdv  32078  topdifinffinlem  32371  icorempt2  32375  isbasisrelowllem1  32379  relowlpssretop  32388  wl-mo3t  32537  poimirlem23  32602  poimirlem29  32608  poimirlem32  32611  poimir  32612  mblfinlem2  32617  sdclem1  32709  fdc  32711  incsequz  32714  rngosn3  32893  0rngo  32996  dmncan1  33045  bicomdd  33153  prtlem15  33178  lsatcvat  33355  lfl1  33375  hlrelat2  33707  cvrat  33726  linepsubN  34056  2llnma3r  34092  dihjatcclem4  35728  dochexmidlem1  35767  rngunsnply  36762  mptrcllem  36939  frege124d  37072  frege77  37254  frege116  37293  or3or  37339  clsk1indlem3  37361  ssralv2  37758  truniALT  37772  onfrALTlem3  37780  onfrALTlem2  37782  onfrALTlem1  37784  ax6e2ndeq  37796  stoweidlem62  38955  atbiffatnnb  39728  2reu3  39837  gboge7  40185  gbege6  40187  uhgrvd00  40750  pthdlem2lem  40973  frcond2  41439  copisnmnd  41599  setrec1lem4  42236