Theorem imbitrrid 156

Description: A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.) (Revised by NM, 22-Sep-2013.)

Hypotheses

Ref	Expression
imbitrrid.1	⊢ (𝜑 → 𝜃)
imbitrrid.2	⊢ (𝜒 → (𝜓 ↔ 𝜃))

Assertion

Ref	Expression
imbitrrid	⊢ (𝜒 → (𝜑 → 𝜓))

Proof of Theorem imbitrrid

Step	Hyp	Ref	Expression
1		imbitrrid.1	. 2 ⊢ (𝜑 → 𝜃)
2		imbitrrid.2	. . 3 ⊢ (𝜒 → (𝜓 ↔ 𝜃))
3	2	bicomd 141	. 2 ⊢ (𝜒 → (𝜃 ↔ 𝜓))
4	1, 3	imbitrid 154	1 ⊢ (𝜒 → (𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  syl5ibrcom  157  biimprd  158  nbn2  709  anifpdc  999  limelon  4546  eldifpw  4625  ssonuni  4637  onsucuni2  4713  peano2  4744  limom  4763  elrnmpt1  5035  cnveqb  5246  cnveq0  5247  relcoi1  5322  f1ssf1  5674  ndmfvg  5729  ffvresb  5874  caovord3d  6263  poxp  6472  nnm0r  6757  nnacl  6758  nnacom  6762  nnaass  6763  nndi  6764  nnmass  6765  nnmsucr  6766  nnmcom  6767  brecop  6904  ecopovtrn  6911  ecopovtrng  6914  elpm2r  6945  map0g  6974  fundmen  7100  dom1o  7122  mapxpen  7154  mapunen  7157  phpm  7173  f1vrnfibi  7265  elfir  7313  mulcmpblnq  7742  ordpipqqs  7748  mulcmpblnq0  7818  genpprecll  7888  genppreclu  7889  addcmpblnr  8113  ax1rid  8251  axpre-mulgt0  8261  cnegexlem1  8509  msqge0  8953  mulge0  8956  ltleap  8969  nnmulcl  9335  nnsub  9353  elnn0z  9667  ztri3or0  9696  nneoor  9759  uz11  9961  xltnegi  10254  frec2uzuzd  10860  seq3fveq2  10933  seqfveq2g  10935  seq3shft2  10939  seqshft2g  10940  seq3split  10946  seqsplitg  10947  seq3caopr3  10949  seqcaopr3g  10950  seqf1oglem2a  10976  seq3id2  10984  seq3homo  10985  seqhomog  10988  m1expcl2  11019  expadd  11039  expmul  11042  faclbnd  11201  hashfzp1  11287  hashmap  11290  hashfacen  11306  hashf1lem2  11308  hashf1  11309  seq3coll  11316  wrdsymb0  11359  len0nnbi  11361  wrd2ind  11517  pfxccatin12lem2c  11524  pfxccatin12lem2  11525  swrdccatin1d  11537  caucvgrelemcau  11768  recan  11898  rexanre  12009  fsumiun  12269  efexp  12474  dvdstr  12620  alzdvds  12646  zob  12683  bitsinv1  12754  gcdmultiplez  12823  dvdssq  12833  cncongr2  12907  prmdiveq  13043  pythagtriplem2  13074  pcexp  13117  elrestr  13660  ptex  13677  xpsff1o  13729  dfgrp3me  13964  mulgneg2  14018  mulgnnass  14019  mhmmulg  14025  gsum2dfilem2  14272  rngpropd  14361  ringadd2  14439  mulgass2  14470  opprrngbg  14492  opprsubrngg  14628  subrngpropd  14633  subrgpropd  14670  rhmpropd  14671  lmodprop2d  14794  cnfldmulg  15022  cnfldexp  15023  assapropd  15123  restopn2  15442  txcn  15534  txlm  15538  isxms2  15711  rpcxpmul2  16179  chtqub  16329  gausslemma2dlem0i  16414  incistruhgr  16569  upgredg2vtx  16627  upgredgpr  16628  uhgr2edg  16685  wlkres  16858  clwwlknonex2  16918  eupth2lem3lem6fi  16950  bj-om  17201  bj-inf2vnlem2  17235  bj-inf2vn  17238  bj-inf2vn2  17239