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  1484  exlimd  2216  cbvexdw  2340  ax13lem2  2379  cbvexd  2411  axc14  2466  mo3  2562  2eu3  2652  2eu6  2655  necon2bd  2954  necon2d  2961  necon4d  2962  spcimgfi1OLD  3548  spc3egv  3603  elabgt  3672  elabgtOLD  3673  reupick  4335  prneimg  4859  dfiun2g  5035  invdisj  5134  trin  5277  exexneq  5445  pwssun  5580  wefrc  5683  eqbrrdva  5883  elreldm  5949  elinxp  6039  xp11  6197  ssrnres  6200  suc11  6493  opelf  6770  dffo4  7123  onmindif2  7827  dftpos3  8268  frrlem13  8322  swoer  8775  domtriord  9162  nneneq  9244  nneneqOLD  9256  unblem1  9326  supnub  9500  infnlb  9530  en3lplem2  9651  suc11reg  9657  inf3lem2  9667  trcl  9766  tz9.13  9829  acndom  10089  carduniima  10134  cardinfima  10135  dfac5lem5  10165  fin23lem26  10363  hsmexlem2  10465  axcc4  10477  axdc3lem2  10489  axdclem2  10558  entric  10595  alephval2  10610  cfpwsdom  10622  fpwwe2lem8  10676  ltapr  11083  supsrlem  11149  sup2  12222  nnunb  12520  nneo  12700  indstr  12956  mul2lt0bi  13139  ngtmnft  13205  qsqueeze  13240  qextlt  13242  qextle  13243  icoshft  13510  injresinj  13824  swrdccatin2  14764  rexuzre  15388  rexico  15389  summo  15750  rpnnen2lem12  16258  divalglem5  16431  ndvdssub  16443  isprm7  16742  prmdvdsncoprmbd  16761  pc2dvds  16913  infpn2  16947  vdwnnlem3  17031  mreiincl  17641  intopsn  18680  pmtrrn2  19493  psgnunilem4  19530  ablfac1eulem  20107  lbsextlem3  21180  xrsdsreclb  21449  znleval  21591  elcls3  23107  isclo2  23112  tgcn  23276  cnprest  23313  ordthaus  23408  hauscmplem  23430  comppfsc  23556  kgencn2  23581  prdstopn  23652  xkohaus  23677  qtoptop2  23723  tgqtop  23736  filufint  23944  fclsbas  24045  alexsubALTlem3  24073  alexsubALTlem4  24074  ptcmplem2  24077  cldsubg  24135  isucn2  24304  metequiv2  24539  bcthlem5  25376  vieta1  26369  aannenlem2  26386  ulmbdd  26456  angpined  26888  rlimcnp2  27024  amgm  27049  ftalem3  27133  bposlem6  27348  nofv  27717  sltres  27722  nogt01o  27756  nosupprefixmo  27760  noinfprefixmo  27761  noetasuplem4  27796  uhgrvd00  29567  pthdlem2lem  29800  frcond2  30296  lnon0  30827  ocnel  31327  h1dn0  31581  cnlnssadj  32109  cvnbtwn2  32316  cvnbtwn3  32317  cvnbtwn4  32318  dmdbr2  32332  dmdbr3  32334  dmdbr4  32335  superpos  32383  atcvati  32415  mdsymlem4  32435  sumdmdii  32444  cdj3lem1  32463  elicoelioo  32787  archiabl  33188  elrgspnlem4  33235  bnj1280  35013  cusgr3cyclex  35121  loop1cycl  35122  erdszelem9  35184  satfvsucsuc  35350  untangtr  35694  dfon2lem6  35770  dfon2lem7  35771  outsideofrflx  36109  trer  36299  elicc3  36300  nn0prpw  36306  bj-syl66ib  36538  bj-cbvexdv  36783  bj-sblem1  36825  bj-spcimdv  36878  bj-spcimdvv  36879  topdifinffinlem  37330  icorempo  37334  isbasisrelowllem1  37338  relowlpssretop  37347  difunieq  37357  fvineqsneq  37395  wl-mo3t  37557  poimirlem23  37630  poimirlem29  37636  poimirlem32  37639  poimir  37640  mblfinlem2  37645  sdclem1  37730  fdc  37732  incsequz  37735  rngosn3  37911  0rngo  38014  dmncan1  38063  disjdmqscossss  38785  bicomdd  38836  prtlem15  38857  lsatcvat  39032  lfl1  39052  hlrelat2  39386  cvrat  39405  linepsubN  39735  2llnma3r  39771  dihjatcclem4  41404  dochexmidlem1  41443  sn-sup2  42478  rngunsnply  43158  onsupuni  43218  tfsconcatrn  43332  mptrcllem  43603  frege124d  43751  frege77  43930  frege116  43969  or3or  44013  clsk1indlem3  44033  ssralv2  44529  truniALT  44539  onfrALTlem3  44542  onfrALTlem2  44544  onfrALTlem1  44546  ax6e2ndeq  44557  stoweidlem62  46018  atbiffatnnb  46862  2reu3  47060  2reuimp  47065  gbowge7  47688  gbege6  47690  copisnmnd  48013  line2ylem  48601  line2xlem  48603  setrec1lem4  48921