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  4808  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  8264  frrlem13  8319  swoer  8752  domtriord  9145  nneneq  9224  unblem1  9287  supnub  9457  infnlb  9488  en3lplem2  9617  suc11reg  9623  inf3lem2  9633  trcl  9732  tz9.13  9801  rankval4b  9883  rankfilimbi  9905  setrec1lem4  9974  acndom  10133  carduniima  10178  cardinfima  10179  dfac5lem5  10209  fin23lem26  10406  hsmexlem2  10508  axcc4  10520  axdc3lem2  10532  axdclem2  10601  entric  10644  alephval2  10660  cfpwsdom  10672  fpwwe2lem8  10726  ltapr  11133  supsrlem  11199  sup2  12276  nnunb  12605  nneo  12786  indstr  13046  mul2lt0bi  13231  ngtmnft  13299  qsqueeze  13334  qextlt  13336  qextle  13337  icoshft  13607  injresinj  13929  swrdccatin2  14882  rexuzre  15525  rexico  15526  summo  15888  rpnnen2lem12  16398  divalglem5  16572  ndvdssub  16584  isprm7  16889  prmdvdsncoprmbd  16908  pc2dvds  17062  infpn2  17096  vdwnnlem3  17180  mreiincl  17771  intopsn  18837  pmtrrn2  19679  psgnunilem4  19716  ablfac1eulem  20293  lbsextlem3  21443  xrsdsreclb  21725  znleval  21865  elcls3  23406  isclo2  23411  tgcn  23575  cnprest  23612  ordthaus  23707  hauscmplem  23729  comppfsc  23856  kgencn2  23881  prdstopn  23952  xkohaus  23977  qtoptop2  24023  tgqtop  24036  filufint  24244  fclsbas  24345  alexsubALTlem3  24373  alexsubALTlem4  24374  ptcmplem2  24377  cldsubg  24435  isucn2  24602  metequiv2  24834  bcthlem5  25654  vieta1  26640  aannenlem2  26661  ulmbdd  26730  angpined  27163  rlimcnp2  27299  amgm  27323  ftalem3  27407  bposlem6  27621  nofv  28019  ltsres  28024  nogt01o  28058  nosupprefixmo  28062  noinfprefixmo  28063  noetasuplem4  28098  z12zsodd  28873  uhgrvd00  30120  pthdlem2lem  30358  loop1cycl  30749  frcond2  30873  lnon0  31405  ocnel  31905  h1dn0  32159  cnlnssadj  32687  cvnbtwn2  32894  cvnbtwn3  32895  cvnbtwn4  32896  dmdbr2  32910  dmdbr3  32912  dmdbr4  32913  superpos  32961  atcvati  32993  mdsymlem4  33013  sumdmdii  33022  cdj3lem1  33041  elicoelioo  33416  archiabl  33805  elrgspnlem4  33852  bnj1280  35696  ordunmax  35765  tz9.1regs  35858  onvfowev  35969  cusgr3cyclex  35987  erdszelem9  36050  satfvsucsuc  36216  untangtr  36571  dfon2lem6  36642  dfon2lem7  36643  outsideofrflx  36984  trer  37196  elicc3  37197  nn0prpw  37203  bj-syl66ib  37516  bj-cbvexdv  37804  bj-sblem1  37846  bj-spcimdv  37899  bj-spcimdvv  37900  bj-axseprep  38082  topdifinffinlem  38363  icorempo  38367  isbasisrelowllem1  38371  relowlpssretop  38380  difunieq  38390  fvineqsneq  38428  wl-mo3t  38601  poimirlem23  38654  poimirlem29  38660  poimirlem32  38663  poimir  38664  mblfinlem2  38669  findcard4  38725  sdclem1  38770  fdc  38772  incsequz  38775  rngosn3  38951  0rngo  39054  dmncan1  39103  sucmapleftuniq  39515  preuniqval  39521  disjdmqscossss  39931  bicomdd  40004  prtlem15  40025  lsatcvat  40200  lfl1  40220  hlrelat2  40553  cvrat  40572  linepsubN  40902  2llnma3r  40938  dihjatcclem4  42571  dochexmidlem1  42610  sn-sup2  43648  rngunsnply  44264  onsupuni  44324  tfsconcatrn  44437  mptrcllem  44706  frege124d  44854  frege77  45033  frege116  45072  or3or  45116  clsk1indlem3  45136  ssralv2  45607  truniALT  45617  onfrALTlem3  45620  onfrALTlem2  45622  onfrALTlem1  45624  ax6e2ndeq  45635  cocanss2  46015  stoweidlem62  47165  atbiffatnnb  48075  2reu3  48273  2reuimp  48278  gbowge7  48954  gbege6  48956  copisnmnd  49359  idomcanl  49537  line2ylem  49956  line2xlem  49958