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 ⊢ (𝜒 → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  syl5ibrcom  157  biimprd  158  nbn2  702  anifpdc  992  limelon  4491  eldifpw  4569  ssonuni  4581  onsucuni2  4657  peano2  4688  limom  4707  elrnmpt1  4978  cnveqb  5187  cnveq0  5188  relcoi1  5263  ndmfvg  5663  ffvresb  5803  caovord3d  6185  poxp  6389  nnm0r  6638  nnacl  6639  nnacom  6643  nnaass  6644  nndi  6645  nnmass  6646  nnmsucr  6647  nnmcom  6648  brecop  6785  ecopovtrn  6792  ecopovtrng  6795  elpm2r  6826  map0g  6848  fundmen  6972  dom1o  6990  mapxpen  7022  phpm  7040  f1vrnfibi  7128  elfir  7156  mulcmpblnq  7571  ordpipqqs  7577  mulcmpblnq0  7647  genpprecll  7717  genppreclu  7718  addcmpblnr  7942  ax1rid  8080  axpre-mulgt0  8090  cnegexlem1  8337  msqge0  8779  mulge0  8782  ltleap  8795  nnmulcl  9147  nnsub  9165  elnn0z  9475  ztri3or0  9504  nneoor  9565  uz11  9762  xltnegi  10048  frec2uzuzd  10641  seq3fveq2  10714  seqfveq2g  10716  seq3shft2  10720  seqshft2g  10721  seq3split  10727  seqsplitg  10728  seq3caopr3  10730  seqcaopr3g  10731  seqf1oglem2a  10757  seq3id2  10765  seq3homo  10766  seqhomog  10769  m1expcl2  10800  expadd  10820  expmul  10823  faclbnd  10980  hashfzp1  11064  hashfacen  11076  seq3coll  11082  wrdsymb0  11122  len0nnbi  11124  wrd2ind  11276  pfxccatin12lem2c  11283  pfxccatin12lem2  11284  swrdccatin1d  11296  caucvgrelemcau  11512  recan  11641  rexanre  11752  fsumiun  12009  efexp  12214  dvdstr  12360  alzdvds  12386  zob  12423  bitsinv1  12494  gcdmultiplez  12563  dvdssq  12573  cncongr2  12647  prmdiveq  12779  pythagtriplem2  12810  pcexp  12853  elrestr  13301  ptex  13318  xpsff1o  13403  dfgrp3me  13654  mulgneg2  13714  mulgnnass  13715  mhmmulg  13721  rngpropd  13939  ringadd2  14011  mulgass2  14042  opprrngbg  14062  opprsubrngg  14196  subrngpropd  14201  subrgpropd  14238  rhmpropd  14239  lmodprop2d  14333  cnfldmulg  14561  cnfldexp  14562  restopn2  14878  txcn  14970  txlm  14974  isxms2  15147  rpcxpmul2  15608  gausslemma2dlem0i  15757  incistruhgr  15911  upgredg2vtx  15967  upgredgpr  15968  uhgr2edg  16025  wlkres  16149  bj-om  16409  bj-inf2vnlem2  16443  bj-inf2vn  16446  bj-inf2vn2  16447