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  1516  exlimd  2254  cbvexdw  2371  ax13lem2  2408  cbvexd  2440  axc14  2495  mo3  2592  2eu3  2681  2eu6  2684  necon2bd  2974  necon2d  2981  necon4d  2982  spcimgfi1OLD  3517  spc3egv  3563  elabgtOLD  3633  reupick  4283  prneimg  4820  dfiun2g  4995  invdisj  5096  trin  5231  exexneq  5418  pwssun  5555  wefrc  5657  eqbrrdva  5857  elreldm  5927  elinxp  6020  xp11  6175  ssrnres  6178  suc11  6472  opelf  6741  dffo4  7100  onmindif2  7807  dftpos3  8241  frrlem13  8296  swoer  8727  domtriord  9112  nneneq  9191  unblem1  9253  supnub  9423  infnlb  9454  en3lplem2  9583  suc11reg  9589  inf3lem2  9599  trcl  9698  tz9.13  9764  acndom  10036  carduniima  10081  cardinfima  10082  dfac5lem5  10112  fin23lem26  10310  hsmexlem2  10412  axcc4  10424  axdc3lem2  10436  axdclem2  10505  entric  10542  alephval2  10558  cfpwsdom  10570  fpwwe2lem8  10624  ltapr  11031  supsrlem  11097  sup2  12172  nnunb  12501  nneo  12681  indstr  12941  mul2lt0bi  13125  ngtmnft  13193  qsqueeze  13228  qextlt  13230  qextle  13231  icoshft  13501  injresinj  13822  swrdccatin2  14768  rexuzre  15406  rexico  15407  summo  15770  rpnnen2lem12  16282  divalglem5  16456  ndvdssub  16468  isprm7  16768  prmdvdsncoprmbd  16787  pc2dvds  16940  infpn2  16974  vdwnnlem3  17058  mreiincl  17649  intopsn  18713  pmtrrn2  19531  psgnunilem4  19568  ablfac1eulem  20145  lbsextlem3  21265  xrsdsreclb  21545  znleval  21685  elcls3  23221  isclo2  23226  tgcn  23390  cnprest  23427  ordthaus  23522  hauscmplem  23544  comppfsc  23670  kgencn2  23695  prdstopn  23766  xkohaus  23791  qtoptop2  23837  tgqtop  23850  filufint  24058  fclsbas  24159  alexsubALTlem3  24187  alexsubALTlem4  24188  ptcmplem2  24191  cldsubg  24249  isucn2  24416  metequiv2  24648  bcthlem5  25468  vieta1  26454  aannenlem2  26473  ulmbdd  26542  angpined  26976  rlimcnp2  27112  amgm  27136  ftalem3  27220  bposlem6  27434  nofv  27802  ltsres  27807  nogt01o  27841  nosupprefixmo  27845  noinfprefixmo  27846  noetasuplem4  27881  z12zsodd  28656  uhgrvd00  29865  pthdlem2lem  30097  frcond2  30599  lnon0  31131  ocnel  31631  h1dn0  31885  cnlnssadj  32413  cvnbtwn2  32620  cvnbtwn3  32621  cvnbtwn4  32622  dmdbr2  32636  dmdbr3  32638  dmdbr4  32639  superpos  32687  atcvati  32719  mdsymlem4  32739  sumdmdii  32748  cdj3lem1  32767  elicoelioo  33104  archiabl  33499  elrgspnlem4  33546  bnj1280  35389  rankval4b  35474  rankfilimbi  35476  tz9.1regs  35528  onvfowev  35581  cusgr3cyclex  35609  loop1cycl  35610  erdszelem9  35672  satfvsucsuc  35838  untangtr  36187  dfon2lem6  36259  dfon2lem7  36260  outsideofrflx  36600  trer  36808  elicc3  36809  nn0prpw  36815  bj-syl66ib  37128  bj-cbvexdv  37416  bj-sblem1  37458  bj-spcimdv  37511  bj-spcimdvv  37512  bj-axseprep  37692  topdifinffinlem  37974  icorempo  37978  isbasisrelowllem1  37982  relowlpssretop  37991  difunieq  38001  fvineqsneq  38039  wl-mo3t  38212  poimirlem23  38275  poimirlem29  38281  poimirlem32  38284  poimir  38285  mblfinlem2  38290  sdclem1  38375  fdc  38377  incsequz  38380  rngosn3  38556  0rngo  38659  dmncan1  38708  sucmapleftuniq  39120  preuniqval  39126  disjdmqscossss  39536  bicomdd  39609  prtlem15  39630  lsatcvat  39805  lfl1  39825  hlrelat2  40158  cvrat  40177  linepsubN  40507  2llnma3r  40543  dihjatcclem4  42176  dochexmidlem1  42215  sn-sup2  43246  rngunsnply  43879  onsupuni  43939  tfsconcatrn  44052  mptrcllem  44322  frege124d  44470  frege77  44649  frege116  44688  or3or  44732  clsk1indlem3  44752  ssralv2  45223  truniALT  45233  onfrALTlem3  45236  onfrALTlem2  45238  onfrALTlem1  45240  ax6e2ndeq  45251  stoweidlem62  46759  atbiffatnnb  47632  2reu3  47830  2reuimp  47835  gbowge7  48511  gbege6  48513  copisnmnd  48917  idomcanl  49095  line2ylem  49514  line2xlem  49516  setrec1lem4  50451