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  3orel2OLD  1516  exlimd  2255  cbvexdw  2369  ax13lem2  2406  cbvexd  2438  axc14  2493  mo3  2590  2eu3  2679  2eu6  2682  necon2bd  2972  necon2d  2979  necon4d  2980  spc3egv  3558  elabgtOLD  3627  reupick  4275  prneimg  4814  dfiun2g  4988  invdisj  5089  trin  5224  exexneq  5403  pwssun  5543  wefrc  5645  eqbrrdva  5847  elreldm  5917  elinxp  6010  xp11  6166  ssrnres  6169  suc11  6465  opelf  6735  dffo4  7095  onmindif2  7810  dftpos3  8245  frrlem13  8300  swoer  8733  domtriord  9126  nneneq  9205  unblem1  9268  supnub  9438  infnlb  9469  en3lplem2  9598  suc11reg  9604  inf3lem2  9614  trcl  9713  tz9.13  9781  rankval4b  9861  rankfilimbi  9883  setrec1lem4  9952  acndom  10111  carduniima  10156  cardinfima  10157  dfac5lem5  10187  fin23lem26  10384  hsmexlem2  10486  axcc4  10498  axdc3lem2  10510  axdclem2  10579  entric  10622  alephval2  10638  cfpwsdom  10650  fpwwe2lem8  10704  ltapr  11111  supsrlem  11177  sup2  12254  nnunb  12583  nneo  12764  indstr  13024  mul2lt0bi  13209  ngtmnft  13277  qsqueeze  13312  qextlt  13314  qextle  13315  icoshft  13585  injresinj  13906  swrdccatin2  14858  rexuzre  15500  rexico  15501  summo  15863  rpnnen2lem12  16373  divalglem5  16547  ndvdssub  16559  isprm7  16864  prmdvdsncoprmbd  16883  pc2dvds  17037  infpn2  17071  vdwnnlem3  17155  mreiincl  17746  intopsn  18812  pmtrrn2  19654  psgnunilem4  19691  ablfac1eulem  20268  lbsextlem3  21418  xrsdsreclb  21700  znleval  21840  elcls3  23381  isclo2  23386  tgcn  23550  cnprest  23587  ordthaus  23682  hauscmplem  23704  comppfsc  23831  kgencn2  23856  prdstopn  23927  xkohaus  23952  qtoptop2  23998  tgqtop  24011  filufint  24219  fclsbas  24320  alexsubALTlem3  24348  alexsubALTlem4  24349  ptcmplem2  24352  cldsubg  24410  isucn2  24577  metequiv2  24809  bcthlem5  25629  vieta1  26617  aannenlem2  26638  ulmbdd  26707  angpined  27140  rlimcnp2  27276  amgm  27300  ftalem3  27384  bposlem6  27598  nofv  27996  ltsres  28001  nogt01o  28035  nosupprefixmo  28039  noinfprefixmo  28040  noetasuplem4  28075  z12zsodd  28850  uhgrvd00  30097  pthdlem2lem  30335  loop1cycl  30726  frcond2  30850  lnon0  31382  ocnel  31882  h1dn0  32136  cnlnssadj  32664  cvnbtwn2  32871  cvnbtwn3  32872  cvnbtwn4  32873  dmdbr2  32887  dmdbr3  32889  dmdbr4  32890  superpos  32938  atcvati  32970  mdsymlem4  32990  sumdmdii  32999  cdj3lem1  33018  elicoelioo  33352  archiabl  33741  elrgspnlem4  33788  bnj1280  35633  tz9.1regs  35775  onvfowev  35868  cusgr3cyclex  35880  erdszelem9  35933  satfvsucsuc  36099  untangtr  36448  dfon2lem6  36520  dfon2lem7  36521  outsideofrflx  36862  trer  37074  elicc3  37075  nn0prpw  37081  bj-syl66ib  37394  bj-cbvexdv  37682  bj-sblem1  37724  bj-spcimdv  37777  bj-spcimdvv  37778  bj-axseprep  37958  topdifinffinlem  38238  icorempo  38242  isbasisrelowllem1  38246  relowlpssretop  38255  difunieq  38265  fvineqsneq  38303  wl-mo3t  38476  poimirlem23  38529  poimirlem29  38535  poimirlem32  38538  poimir  38539  mblfinlem2  38544  findcard4  38600  sdclem1  38645  fdc  38647  incsequz  38650  rngosn3  38826  0rngo  38929  dmncan1  38978  sucmapleftuniq  39390  preuniqval  39396  disjdmqscossss  39806  bicomdd  39879  prtlem15  39900  lsatcvat  40075  lfl1  40095  hlrelat2  40428  cvrat  40447  linepsubN  40777  2llnma3r  40813  dihjatcclem4  42446  dochexmidlem1  42485  sn-sup2  43523  rngunsnply  44129  onsupuni  44189  tfsconcatrn  44302  mptrcllem  44572  frege124d  44720  frege77  44899  frege116  44938  or3or  44982  clsk1indlem3  45002  ssralv2  45473  truniALT  45483  onfrALTlem3  45486  onfrALTlem2  45488  onfrALTlem1  45490  ax6e2ndeq  45501  stoweidlem62  47016  atbiffatnnb  47926  2reu3  48124  2reuimp  48129  gbowge7  48805  gbege6  48807  copisnmnd  49210  idomcanl  49388  line2ylem  49807  line2xlem  49809