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 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  3imtr3g  298  3orel2OLD  1509  exlimd  2256  cbvexdw  2373  ax13lem2  2410  cbvexd  2442  axc14  2497  mo3  2594  2eu3  2683  2eu6  2686  necon2bd  2976  necon2d  2983  necon4d  2984  spcimgfi1OLD  3519  spc3egv  3565  elabgtOLD  3635  reupick  4284  prneimg  4815  dfiun2g  4990  invdisj  5091  trin  5224  exexneq  5407  pwssun  5544  wefrc  5646  eqbrrdva  5846  elreldm  5916  elinxp  6009  xp11  6165  ssrnres  6168  suc11  6459  opelf  6729  dffo4  7088  onmindif2  7794  dftpos3  8228  frrlem13  8283  swoer  8714  domtriord  9099  nneneq  9178  unblem1  9240  supnub  9410  infnlb  9441  en3lplem2  9570  suc11reg  9576  inf3lem2  9586  trcl  9685  tz9.13  9751  acndom  10023  carduniima  10068  cardinfima  10069  dfac5lem5  10099  fin23lem26  10297  hsmexlem2  10399  axcc4  10411  axdc3lem2  10423  axdclem2  10492  entric  10529  alephval2  10545  cfpwsdom  10557  fpwwe2lem8  10611  ltapr  11018  supsrlem  11084  sup2  12162  nnunb  12491  nneo  12671  indstr  12931  mul2lt0bi  13115  ngtmnft  13183  qsqueeze  13218  qextlt  13220  qextle  13221  icoshft  13491  injresinj  13811  swrdccatin2  14756  rexuzre  15394  rexico  15395  summo  15758  rpnnen2lem12  16271  divalglem5  16445  ndvdssub  16457  isprm7  16757  prmdvdsncoprmbd  16776  pc2dvds  16929  infpn2  16963  vdwnnlem3  17047  mreiincl  17638  intopsn  18702  pmtrrn2  19521  psgnunilem4  19558  ablfac1eulem  20135  lbsextlem3  21253  xrsdsreclb  21524  znleval  21664  elcls3  23201  isclo2  23206  tgcn  23370  cnprest  23407  ordthaus  23502  hauscmplem  23524  comppfsc  23650  kgencn2  23675  prdstopn  23746  xkohaus  23771  qtoptop2  23817  tgqtop  23830  filufint  24038  fclsbas  24139  alexsubALTlem3  24167  alexsubALTlem4  24168  ptcmplem2  24171  cldsubg  24229  isucn2  24396  metequiv2  24628  bcthlem5  25448  vieta1  26434  aannenlem2  26451  ulmbdd  26519  angpined  26953  rlimcnp2  27089  amgm  27113  ftalem3  27197  bposlem6  27411  nofv  27779  ltsres  27784  nogt01o  27818  nosupprefixmo  27822  noinfprefixmo  27823  noetasuplem4  27858  z12zsodd  28633  uhgrvd00  29793  pthdlem2lem  30025  frcond2  30527  lnon0  31059  ocnel  31559  h1dn0  31813  cnlnssadj  32341  cvnbtwn2  32548  cvnbtwn3  32549  cvnbtwn4  32550  dmdbr2  32564  dmdbr3  32566  dmdbr4  32567  superpos  32615  atcvati  32647  mdsymlem4  32667  sumdmdii  32676  cdj3lem1  32695  elicoelioo  33035  archiabl  33431  elrgspnlem4  33478  bnj1280  35325  rankval4b  35408  rankfilimbi  35409  tz9.1regs  35442  onvfowev  35471  cusgr3cyclex  35499  loop1cycl  35500  erdszelem9  35562  satfvsucsuc  35728  untangtr  36077  dfon2lem6  36149  dfon2lem7  36150  outsideofrflx  36490  trer  36689  elicc3  36690  nn0prpw  36696  bj-syl66ib  37009  bj-cbvexdv  37297  bj-sblem1  37339  bj-spcimdv  37392  bj-spcimdvv  37393  bj-axseprep  37571  topdifinffinlem  37853  icorempo  37857  isbasisrelowllem1  37861  relowlpssretop  37870  difunieq  37880  fvineqsneq  37918  wl-mo3t  38091  poimirlem23  38154  poimirlem29  38160  poimirlem32  38163  poimir  38164  mblfinlem2  38169  sdclem1  38254  fdc  38256  incsequz  38259  rngosn3  38435  0rngo  38538  dmncan1  38587  sucmapleftuniq  39001  preuniqval  39007  disjdmqscossss  39417  bicomdd  39490  prtlem15  39511  lsatcvat  39686  lfl1  39706  hlrelat2  40039  cvrat  40058  linepsubN  40388  2llnma3r  40424  dihjatcclem4  42057  dochexmidlem1  42096  sn-sup2  43125  rngunsnply  43758  onsupuni  43818  tfsconcatrn  43931  mptrcllem  44201  frege124d  44349  frege77  44528  frege116  44567  or3or  44611  clsk1indlem3  44631  ssralv2  45105  truniALT  45115  onfrALTlem3  45118  onfrALTlem2  45120  onfrALTlem1  45122  ax6e2ndeq  45133  stoweidlem62  46634  atbiffatnnb  47504  2reu3  47702  2reuimp  47707  gbowge7  48383  gbege6  48385  copisnmnd  48789  line2ylem  49382  line2xlem  49384  setrec1lem4  50319