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  exlimd  2214  cbvexdw  2338  ax13lem2  2376  cbvexd  2408  axc14  2463  mo3  2564  2eu3  2655  2eu6  2658  necon2bd  2958  necon2d  2965  necon4d  2966  vtoclgft  3482  spcimgft  3516  spc3egv  3532  elabgt  3596  reupick  4249  prneimg  4782  invdisj  5054  trin  5197  pwssun  5476  wefrc  5574  eqbrrdva  5767  elreldm  5833  elinxp  5918  xp11  6067  ssrnres  6070  suc11  6354  opelf  6619  dffo4  6961  onmindif2  7634  dftpos3  8031  frrlem13  8085  swoer  8486  domtriord  8859  nneneq  8896  unblem1  8996  supnub  9151  infnlb  9181  en3lplem2  9301  suc11reg  9307  inf3lem2  9317  trcl  9417  tz9.13  9480  acndom  9738  carduniima  9783  cardinfima  9784  dfac5lem5  9814  fin23lem26  10012  hsmexlem2  10114  axcc4  10126  axdc3lem2  10138  axdclem2  10207  entric  10244  alephval2  10259  cfpwsdom  10271  fpwwe2lem8  10325  ltapr  10732  supsrlem  10798  sup2  11861  nnunb  12159  nneo  12334  indstr  12585  mul2lt0bi  12765  ngtmnft  12829  qsqueeze  12864  qextlt  12866  qextle  12867  icoshft  13134  injresinj  13436  swrdccatin2  14370  rexuzre  14992  rexico  14993  summo  15357  rpnnen2lem12  15862  divalglem5  16034  ndvdssub  16046  isprm7  16341  prmdvdsncoprmbd  16359  pc2dvds  16508  infpn2  16542  vdwnnlem3  16626  mreiincl  17222  intopsn  18253  pmtrrn2  18983  psgnunilem4  19020  ablfac1eulem  19590  lbsextlem3  20337  xrsdsreclb  20557  znleval  20674  elcls3  22142  isclo2  22147  tgcn  22311  cnprest  22348  ordthaus  22443  hauscmplem  22465  comppfsc  22591  kgencn2  22616  prdstopn  22687  xkohaus  22712  qtoptop2  22758  tgqtop  22771  filufint  22979  fclsbas  23080  alexsubALTlem3  23108  alexsubALTlem4  23109  ptcmplem2  23112  cldsubg  23170  isucn2  23339  metequiv2  23572  bcthlem5  24397  vieta1  25377  aannenlem2  25394  ulmbdd  25462  angpined  25885  rlimcnp2  26021  amgm  26045  ftalem3  26129  bposlem6  26342  uhgrvd00  27804  pthdlem2lem  28036  frcond2  28532  lnon0  29061  ocnel  29561  h1dn0  29815  cnlnssadj  30343  cvnbtwn2  30550  cvnbtwn3  30551  cvnbtwn4  30552  dmdbr2  30566  dmdbr3  30568  dmdbr4  30569  superpos  30617  atcvati  30649  mdsymlem4  30669  sumdmdii  30678  cdj3lem1  30697  elicoelioo  31001  archiabl  31354  bnj1280  32900  cusgr3cyclex  32998  loop1cycl  32999  erdszelem9  33061  satfvsucsuc  33227  untangtr  33555  3orel2  33556  dfon2lem6  33670  dfon2lem7  33671  nofv  33787  sltres  33792  nogt01o  33826  nosupprefixmo  33830  noinfprefixmo  33831  noetasuplem4  33866  outsideofrflx  34356  trer  34432  elicc3  34433  nn0prpw  34439  bj-syl66ib  34662  bj-cbvexdv  34909  bj-sblem1  34953  bj-spcimdv  35007  bj-spcimdvv  35008  topdifinffinlem  35445  icorempo  35449  isbasisrelowllem1  35453  relowlpssretop  35462  difunieq  35472  fvineqsneq  35510  wl-mo3t  35658  poimirlem23  35727  poimirlem29  35733  poimirlem32  35736  poimir  35737  mblfinlem2  35742  sdclem1  35828  fdc  35830  incsequz  35833  rngosn3  36009  0rngo  36112  dmncan1  36161  bicomdd  36795  prtlem15  36816  lsatcvat  36991  lfl1  37011  hlrelat2  37344  cvrat  37363  linepsubN  37693  2llnma3r  37729  dihjatcclem4  39362  dochexmidlem1  39401  sn-dtru  40116  sn-sup2  40360  rngunsnply  40914  mptrcllem  41110  frege124d  41258  frege77  41437  frege116  41476  or3or  41520  clsk1indlem3  41542  ssralv2  42040  truniALT  42050  onfrALTlem3  42053  onfrALTlem2  42055  onfrALTlem1  42057  ax6e2ndeq  42068  stoweidlem62  43493  atbiffatnnb  44294  2reu3  44489  2reuimp  44494  gbowge7  45103  gbege6  45105  copisnmnd  45251  line2ylem  45985  line2xlem  45987  setrec1lem4  46282