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  2257  cbvexdw  2374  ax13lem2  2411  cbvexd  2443  axc14  2498  mo3  2595  2eu3  2684  2eu6  2687  necon2bd  2977  necon2d  2984  necon4d  2985  spc3egv  3565  elabgtOLD  3635  reupick  4285  prneimg  4824  dfiun2g  4999  invdisj  5100  trin  5235  exexneq  5421  pwssun  5558  wefrc  5660  eqbrrdva  5860  elreldm  5930  elinxp  6023  xp11  6178  ssrnres  6181  suc11  6477  opelf  6746  dffo4  7105  onmindif2  7815  dftpos3  8249  frrlem13  8304  swoer  8735  domtriord  9121  nneneq  9200  unblem1  9262  supnub  9432  infnlb  9463  en3lplem2  9592  suc11reg  9598  inf3lem2  9608  trcl  9707  tz9.13  9773  acndom  10054  carduniima  10099  cardinfima  10100  dfac5lem5  10130  fin23lem26  10327  hsmexlem2  10429  axcc4  10441  axdc3lem2  10453  axdclem2  10522  entric  10559  alephval2  10575  cfpwsdom  10587  fpwwe2lem8  10641  ltapr  11048  supsrlem  11114  sup2  12189  nnunb  12518  nneo  12698  indstr  12958  mul2lt0bi  13142  ngtmnft  13210  qsqueeze  13245  qextlt  13247  qextle  13248  icoshft  13518  injresinj  13839  swrdccatin2  14790  rexuzre  15430  rexico  15431  summo  15794  rpnnen2lem12  16306  divalglem5  16480  ndvdssub  16492  isprm7  16792  prmdvdsncoprmbd  16811  pc2dvds  16964  infpn2  16998  vdwnnlem3  17082  mreiincl  17673  intopsn  18737  pmtrrn2  19561  psgnunilem4  19598  ablfac1eulem  20175  lbsextlem3  21321  xrsdsreclb  21601  znleval  21741  elcls3  23277  isclo2  23282  tgcn  23446  cnprest  23483  ordthaus  23578  hauscmplem  23600  comppfsc  23726  kgencn2  23751  prdstopn  23822  xkohaus  23847  qtoptop2  23893  tgqtop  23906  filufint  24114  fclsbas  24215  alexsubALTlem3  24243  alexsubALTlem4  24244  ptcmplem2  24247  cldsubg  24305  isucn2  24472  metequiv2  24704  bcthlem5  25524  vieta1  26510  aannenlem2  26529  ulmbdd  26598  angpined  27032  rlimcnp2  27168  amgm  27192  ftalem3  27276  bposlem6  27490  nofv  27858  ltsres  27863  nogt01o  27897  nosupprefixmo  27901  noinfprefixmo  27902  noetasuplem4  27937  z12zsodd  28712  uhgrvd00  29921  pthdlem2lem  30153  frcond2  30655  lnon0  31187  ocnel  31687  h1dn0  31941  cnlnssadj  32469  cvnbtwn2  32676  cvnbtwn3  32677  cvnbtwn4  32678  dmdbr2  32692  dmdbr3  32694  dmdbr4  32695  superpos  32743  atcvati  32775  mdsymlem4  32795  sumdmdii  32804  cdj3lem1  32823  elicoelioo  33160  archiabl  33549  elrgspnlem4  33596  bnj1280  35440  rankval4b  35518  rankfilimbi  35520  tz9.1regs  35571  onvfowev  35624  cusgr3cyclex  35649  loop1cycl  35650  erdszelem9  35712  satfvsucsuc  35878  untangtr  36227  dfon2lem6  36299  dfon2lem7  36300  outsideofrflx  36640  trer  36868  elicc3  36869  nn0prpw  36875  bj-syl66ib  37188  bj-cbvexdv  37476  bj-sblem1  37518  bj-spcimdv  37571  bj-spcimdvv  37572  bj-axseprep  37752  topdifinffinlem  38034  icorempo  38038  isbasisrelowllem1  38042  relowlpssretop  38051  difunieq  38061  fvineqsneq  38099  wl-mo3t  38272  poimirlem23  38335  poimirlem29  38341  poimirlem32  38344  poimir  38345  mblfinlem2  38350  sdclem1  38435  fdc  38437  incsequz  38440  rngosn3  38616  0rngo  38719  dmncan1  38768  sucmapleftuniq  39180  preuniqval  39186  disjdmqscossss  39596  bicomdd  39669  prtlem15  39690  lsatcvat  39865  lfl1  39885  hlrelat2  40218  cvrat  40237  linepsubN  40567  2llnma3r  40603  dihjatcclem4  42236  dochexmidlem1  42275  sn-sup2  43306  rngunsnply  43937  onsupuni  43997  tfsconcatrn  44110  mptrcllem  44380  frege124d  44528  frege77  44707  frege116  44746  or3or  44790  clsk1indlem3  44810  ssralv2  45281  truniALT  45291  onfrALTlem3  45294  onfrALTlem2  45296  onfrALTlem1  45298  ax6e2ndeq  45309  stoweidlem62  46817  atbiffatnnb  47690  2reu3  47888  2reuimp  47893  gbowge7  48569  gbege6  48571  copisnmnd  48975  idomcanl  49153  line2ylem  49572  line2xlem  49574  setrec1lem4  50509