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  698  limelon  4430  eldifpw  4508  ssonuni  4520  onsucuni2  4596  peano2  4627  limom  4646  elrnmpt1  4913  cnveqb  5121  cnveq0  5122  relcoi1  5197  ndmfvg  5585  ffvresb  5721  caovord3d  6089  poxp  6285  nnm0r  6532  nnacl  6533  nnacom  6537  nnaass  6538  nndi  6539  nnmass  6540  nnmsucr  6541  nnmcom  6542  brecop  6679  ecopovtrn  6686  ecopovtrng  6689  elpm2r  6720  map0g  6742  fundmen  6860  mapxpen  6904  phpm  6921  f1vrnfibi  7004  elfir  7032  mulcmpblnq  7428  ordpipqqs  7434  mulcmpblnq0  7504  genpprecll  7574  genppreclu  7575  addcmpblnr  7799  ax1rid  7937  axpre-mulgt0  7947  cnegexlem1  8194  msqge0  8635  mulge0  8638  ltleap  8651  nnmulcl  9003  nnsub  9021  elnn0z  9330  ztri3or0  9359  nneoor  9419  uz11  9615  xltnegi  9901  frec2uzuzd  10473  seq3fveq2  10546  seqfveq2g  10548  seq3shft2  10552  seqshft2g  10553  seq3split  10559  seqsplitg  10560  seq3caopr3  10562  seqcaopr3g  10563  seqf1oglem2a  10589  seq3id2  10597  seq3homo  10598  seqhomog  10601  m1expcl2  10632  expadd  10652  expmul  10655  faclbnd  10812  hashfzp1  10895  hashfacen  10907  seq3coll  10913  wrdsymb0  10946  len0nnbi  10948  caucvgrelemcau  11124  recan  11253  rexanre  11364  fsumiun  11620  efexp  11825  dvdstr  11971  alzdvds  11996  zob  12032  gcdmultiplez  12158  dvdssq  12168  cncongr2  12242  prmdiveq  12374  pythagtriplem2  12404  pcexp  12447  elrestr  12858  ptex  12875  xpsff1o  12932  dfgrp3me  13172  mulgneg2  13226  mulgnnass  13227  mhmmulg  13233  rngpropd  13451  ringadd2  13523  mulgass2  13554  opprrngbg  13574  opprsubrngg  13707  subrngpropd  13712  subrgpropd  13749  rhmpropd  13750  lmodprop2d  13844  cnfldmulg  14064  cnfldexp  14065  restopn2  14351  txcn  14443  txlm  14447  isxms2  14620  gausslemma2dlem0i  15173  bj-om  15429  bj-inf2vnlem2  15463  bj-inf2vn  15466  bj-inf2vn2  15467