Theorem imbitrdi 254

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

Hypotheses

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

Assertion

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

Proof of Theorem imbitrdi

Step	Hyp	Ref	Expression
1		imbitrdi.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		imbitrdi.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
3	2	biimpi 219	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 36	1 ⊢ (𝜑 → (𝜓 → 𝜃))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3imtr3g  298  exlimd  2254  cbvexdw  2368  ax13lem2  2405  cbvexd  2437  axc14  2492  mo3  2589  2eu3  2678  2eu6  2681  necon2bd  2971  necon2d  2978  necon4d  2979  spc3egv  3557  elabgtOLD  3626  reupick  4274  prneimg  4813  dfiun2g  4987  invdisj  5088  trin  5223  exexneq  5402  pwssun  5542  wefrc  5644  eqbrrdva  5846  elreldm  5916  elinxp  6007  xp11  6166  ssrnres  6169  suc11  6472  opelf  6743  dffo4  7103  onmindif2  7821  dftpos3  8261  frrlem13  8316  swoer  8749  domtriord  9142  nneneq  9221  unblem1  9284  supnub  9454  infnlb  9485  en3lplem2  9614  suc11reg  9620  inf3lem2  9630  trcl  9729  tz9.13  9798  rankval4b  9880  rankfilimbi  9902  setrec1lem4  9971  acndom  10130  carduniima  10175  cardinfima  10176  dfac5lem5  10206  fin23lem26  10403  hsmexlem2  10505  axcc4  10517  axdc3lem2  10529  axdclem2  10598  entric  10641  alephval2  10657  cfpwsdom  10669  fpwwe2lem8  10723  ltapr  11130  supsrlem  11196  sup2  12273  nnunb  12602  nneo  12783  indstr  13043  mul2lt0bi  13228  ngtmnft  13296  qsqueeze  13331  qextlt  13333  qextle  13334  icoshft  13604  injresinj  13926  swrdccatin2  14878  rexuzre  15520  rexico  15521  summo  15883  rpnnen2lem12  16393  divalglem5  16567  ndvdssub  16579  isprm7  16884  prmdvdsncoprmbd  16903  pc2dvds  17057  infpn2  17091  vdwnnlem3  17175  mreiincl  17766  intopsn  18832  pmtrrn2  19674  psgnunilem4  19711  ablfac1eulem  20288  lbsextlem3  21438  xrsdsreclb  21720  znleval  21860  elcls3  23401  isclo2  23406  tgcn  23570  cnprest  23607  ordthaus  23702  hauscmplem  23724  comppfsc  23851  kgencn2  23876  prdstopn  23947  xkohaus  23972  qtoptop2  24018  tgqtop  24031  filufint  24239  fclsbas  24340  alexsubALTlem3  24368  alexsubALTlem4  24369  ptcmplem2  24372  cldsubg  24430  isucn2  24597  metequiv2  24829  bcthlem5  25649  vieta1  26635  aannenlem2  26656  ulmbdd  26725  angpined  27158  rlimcnp2  27294  amgm  27318  ftalem3  27402  bposlem6  27616  nofv  28014  ltsres  28019  nogt01o  28053  nosupprefixmo  28057  noinfprefixmo  28058  noetasuplem4  28093  z12zsodd  28868  uhgrvd00  30115  pthdlem2lem  30353  loop1cycl  30744  frcond2  30868  lnon0  31400  ocnel  31900  h1dn0  32154  cnlnssadj  32682  cvnbtwn2  32889  cvnbtwn3  32890  cvnbtwn4  32891  dmdbr2  32905  dmdbr3  32907  dmdbr4  32908  superpos  32956  atcvati  32988  mdsymlem4  33008  sumdmdii  33017  cdj3lem1  33036  elicoelioo  33412  archiabl  33801  elrgspnlem4  33848  bnj1280  35692  tz9.1regs  35844  onvfowev  35941  cusgr3cyclex  35953  erdszelem9  36006  satfvsucsuc  36172  untangtr  36521  dfon2lem6  36592  dfon2lem7  36593  outsideofrflx  36934  trer  37146  elicc3  37147  nn0prpw  37153  bj-syl66ib  37466  bj-cbvexdv  37754  bj-sblem1  37796  bj-spcimdv  37849  bj-spcimdvv  37850  bj-axseprep  38032  topdifinffinlem  38313  icorempo  38317  isbasisrelowllem1  38321  relowlpssretop  38330  difunieq  38340  fvineqsneq  38378  wl-mo3t  38551  poimirlem23  38604  poimirlem29  38610  poimirlem32  38613  poimir  38614  mblfinlem2  38619  findcard4  38675  sdclem1  38720  fdc  38722  incsequz  38725  rngosn3  38901  0rngo  39004  dmncan1  39053  sucmapleftuniq  39465  preuniqval  39471  disjdmqscossss  39881  bicomdd  39954  prtlem15  39975  lsatcvat  40150  lfl1  40170  hlrelat2  40503  cvrat  40522  linepsubN  40852  2llnma3r  40888  dihjatcclem4  42521  dochexmidlem1  42560  sn-sup2  43598  rngunsnply  44213  onsupuni  44273  tfsconcatrn  44386  mptrcllem  44655  frege124d  44803  frege77  44982  frege116  45021  or3or  45065  clsk1indlem3  45085  ssralv2  45556  truniALT  45566  onfrALTlem3  45569  onfrALTlem2  45571  onfrALTlem1  45573  ax6e2ndeq  45584  cocanss2  45964  stoweidlem62  47114  atbiffatnnb  48024  2reu3  48222  2reuimp  48227  gbowge7  48903  gbege6  48905  copisnmnd  49308  idomcanl  49486  line2ylem  49905  line2xlem  49907