Theorem imbitrdi 251

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 216	. 2 ⊢ (𝜒 → 𝜃)
4	1, 3	syl6 35	1 ⊢ (𝜑 → (𝜓 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  3imtr3g  295  3orel2OLD  1487  exlimd  2219  cbvexdw  2341  ax13lem2  2381  cbvexd  2413  axc14  2468  mo3  2564  2eu3  2654  2eu6  2657  necon2bd  2949  necon2d  2956  necon4d  2957  spcimgfi1OLD  3532  spc3egv  3587  elabgt  3656  elabgtOLD  3657  reupick  4309  prneimg  4835  dfiun2g  5011  invdisj  5110  trin  5246  exexneq  5414  pwssun  5550  wefrc  5653  eqbrrdva  5854  elreldm  5920  elinxp  6011  xp11  6169  ssrnres  6172  suc11  6466  opelf  6744  dffo4  7098  onmindif2  7806  dftpos3  8248  frrlem13  8302  swoer  8755  domtriord  9142  nneneq  9225  unblem1  9305  supnub  9479  infnlb  9510  en3lplem2  9632  suc11reg  9638  inf3lem2  9648  trcl  9747  tz9.13  9810  acndom  10070  carduniima  10115  cardinfima  10116  dfac5lem5  10146  fin23lem26  10344  hsmexlem2  10446  axcc4  10458  axdc3lem2  10470  axdclem2  10539  entric  10576  alephval2  10591  cfpwsdom  10603  fpwwe2lem8  10657  ltapr  11064  supsrlem  11130  sup2  12203  nnunb  12502  nneo  12682  indstr  12937  mul2lt0bi  13120  ngtmnft  13187  qsqueeze  13222  qextlt  13224  qextle  13225  icoshft  13495  injresinj  13809  swrdccatin2  14752  rexuzre  15376  rexico  15377  summo  15738  rpnnen2lem12  16248  divalglem5  16421  ndvdssub  16433  isprm7  16732  prmdvdsncoprmbd  16751  pc2dvds  16904  infpn2  16938  vdwnnlem3  17022  mreiincl  17613  intopsn  18637  pmtrrn2  19446  psgnunilem4  19483  ablfac1eulem  20060  lbsextlem3  21126  xrsdsreclb  21386  znleval  21520  elcls3  23026  isclo2  23031  tgcn  23195  cnprest  23232  ordthaus  23327  hauscmplem  23349  comppfsc  23475  kgencn2  23500  prdstopn  23571  xkohaus  23596  qtoptop2  23642  tgqtop  23655  filufint  23863  fclsbas  23964  alexsubALTlem3  23992  alexsubALTlem4  23993  ptcmplem2  23996  cldsubg  24054  isucn2  24222  metequiv2  24454  bcthlem5  25285  vieta1  26277  aannenlem2  26294  ulmbdd  26364  angpined  26797  rlimcnp2  26933  amgm  26958  ftalem3  27042  bposlem6  27257  nofv  27626  sltres  27631  nogt01o  27665  nosupprefixmo  27669  noinfprefixmo  27670  noetasuplem4  27705  uhgrvd00  29519  pthdlem2lem  29754  frcond2  30253  lnon0  30784  ocnel  31284  h1dn0  31538  cnlnssadj  32066  cvnbtwn2  32273  cvnbtwn3  32274  cvnbtwn4  32275  dmdbr2  32289  dmdbr3  32291  dmdbr4  32292  superpos  32340  atcvati  32372  mdsymlem4  32392  sumdmdii  32401  cdj3lem1  32420  elicoelioo  32760  archiabl  33201  elrgspnlem4  33245  bnj1280  35056  cusgr3cyclex  35163  loop1cycl  35164  erdszelem9  35226  satfvsucsuc  35392  untangtr  35736  dfon2lem6  35811  dfon2lem7  35812  outsideofrflx  36150  trer  36339  elicc3  36340  nn0prpw  36346  bj-syl66ib  36578  bj-cbvexdv  36823  bj-sblem1  36865  bj-spcimdv  36918  bj-spcimdvv  36919  topdifinffinlem  37370  icorempo  37374  isbasisrelowllem1  37378  relowlpssretop  37387  difunieq  37397  fvineqsneq  37435  wl-mo3t  37599  poimirlem23  37672  poimirlem29  37678  poimirlem32  37681  poimir  37682  mblfinlem2  37687  sdclem1  37772  fdc  37774  incsequz  37777  rngosn3  37953  0rngo  38056  dmncan1  38105  disjdmqscossss  38826  bicomdd  38877  prtlem15  38898  lsatcvat  39073  lfl1  39093  hlrelat2  39427  cvrat  39446  linepsubN  39776  2llnma3r  39812  dihjatcclem4  41445  dochexmidlem1  41484  sn-sup2  42489  rngunsnply  43168  onsupuni  43228  tfsconcatrn  43341  mptrcllem  43612  frege124d  43760  frege77  43939  frege116  43978  or3or  44022  clsk1indlem3  44042  ssralv2  44531  truniALT  44541  onfrALTlem3  44544  onfrALTlem2  44546  onfrALTlem1  44548  ax6e2ndeq  44559  stoweidlem62  46071  atbiffatnnb  46921  2reu3  47119  2reuimp  47124  gbowge7  47757  gbege6  47759  copisnmnd  48124  line2ylem  48711  line2xlem  48713  setrec1lem4  49534