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  4487  eldifpw  4565  ssonuni  4577  onsucuni2  4653  peano2  4684  limom  4703  elrnmpt1  4971  cnveqb  5180  cnveq0  5181  relcoi1  5256  ndmfvg  5654  ffvresb  5791  caovord3d  6167  poxp  6368  nnm0r  6615  nnacl  6616  nnacom  6620  nnaass  6621  nndi  6622  nnmass  6623  nnmsucr  6624  nnmcom  6625  brecop  6762  ecopovtrn  6769  ecopovtrng  6772  elpm2r  6803  map0g  6825  fundmen  6949  mapxpen  6997  phpm  7015  f1vrnfibi  7100  elfir  7128  mulcmpblnq  7543  ordpipqqs  7549  mulcmpblnq0  7619  genpprecll  7689  genppreclu  7690  addcmpblnr  7914  ax1rid  8052  axpre-mulgt0  8062  cnegexlem1  8309  msqge0  8751  mulge0  8754  ltleap  8767  nnmulcl  9119  nnsub  9137  elnn0z  9447  ztri3or0  9476  nneoor  9537  uz11  9733  xltnegi  10019  frec2uzuzd  10611  seq3fveq2  10684  seqfveq2g  10686  seq3shft2  10690  seqshft2g  10691  seq3split  10697  seqsplitg  10698  seq3caopr3  10700  seqcaopr3g  10701  seqf1oglem2a  10727  seq3id2  10735  seq3homo  10736  seqhomog  10739  m1expcl2  10770  expadd  10790  expmul  10793  faclbnd  10950  hashfzp1  11033  hashfacen  11045  seq3coll  11051  wrdsymb0  11090  len0nnbi  11092  wrd2ind  11241  pfxccatin12lem2c  11248  pfxccatin12lem2  11249  swrdccatin1d  11261  caucvgrelemcau  11477  recan  11606  rexanre  11717  fsumiun  11974  efexp  12179  dvdstr  12325  alzdvds  12351  zob  12388  bitsinv1  12459  gcdmultiplez  12528  dvdssq  12538  cncongr2  12612  prmdiveq  12744  pythagtriplem2  12775  pcexp  12818  elrestr  13266  ptex  13283  xpsff1o  13368  dfgrp3me  13619  mulgneg2  13679  mulgnnass  13680  mhmmulg  13686  rngpropd  13904  ringadd2  13976  mulgass2  14007  opprrngbg  14027  opprsubrngg  14160  subrngpropd  14165  subrgpropd  14202  rhmpropd  14203  lmodprop2d  14297  cnfldmulg  14525  cnfldexp  14526  restopn2  14842  txcn  14934  txlm  14938  isxms2  15111  rpcxpmul2  15572  gausslemma2dlem0i  15721  incistruhgr  15875  upgredg2vtx  15931  upgredgpr  15932  uhgr2edg  15989  bj-om  16230  bj-inf2vnlem2  16264  bj-inf2vn  16267  bj-inf2vn2  16268  dom1o  16286