Theorem biimtrid 241

Description: A mixed syllogism inference from a nested implication and a biconditional. Useful for substituting an embedded antecedent with a definition. (Contributed by NM, 12-Jan-1993.)

Hypotheses

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

Assertion

Ref	Expression
biimtrid	⊢ (𝜒 → (𝜑 → 𝜃))

Proof of Theorem biimtrid

Step	Hyp	Ref	Expression
1		biimtrid.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	biimpi 215	. 2 ⊢ (𝜑 → 𝜓)
3		biimtrid.2	. 2 ⊢ (𝜒 → (𝜓 → 𝜃))
4	2, 3	syl5 34	1 ⊢ (𝜒 → (𝜑 → 𝜃))

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  3imtr4g  296  3orel1  1091  3orel2  1485  3orel3  1486  cad0  1617  ax13  2373  2euexv  2631  2euex  2641  eqneqall  2952  necon3bd  2955  elnelall  3060  spcimgft  3531  rspc  3554  rspcimdv  3556  rspc2gv  3574  euind  3664  reuind  3693  2reurex  3700  sbciegft  3759  rspsbc  3817  elneeldif  3906  ssexnelpss  4054  rspn0  4292  ralnralall  4455  pwpw0  4752  sssn  4765  prnebg  4792  pwsnOLD  4837  intss1  4901  intmin  4906  uniintsn  4925  iinss  4993  iinss2  4994  disji2  5063  disjiun  5068  disjiund  5071  disjxiun  5078  trel3  5208  trin  5210  eusvnfb  5325  reusv3  5337  axprlem2  5356  copsexgw  5417  copsexg  5418  propeqop  5434  otiunsndisj  5447  iunopeqop  5448  po3nr  5529  friOLD  5561  wefrc  5594  wereu2  5597  ssrelrel  5718  relop  5772  iss  5955  poirr2  6044  xpcan  6094  xpcan2  6095  sossfld  6104  frpomin  6258  frpoind  6260  frpoins2fg  6262  wfiOLD  6269  wfis2fgOLD  6275  onfr  6320  onmindif  6372  onun2  6387  iotan0  6448  funopg  6497  funssres  6507  funun  6509  fv3  6822  fvmptt  6927  iinpreima  6978  fvn0ssdmfun  6984  dff3  7008  dff4  7009  fmptsng  7072  fmptsnd  7073  tpres  7108  fnprb  7116  fntpb  7117  fvclss  7147  fpropnf1  7172  isomin  7240  isofrlem  7243  weniso  7257  oprabidw  7338  oprabid  7339  ssorduni  7661  onmindif2  7689  limuni3  7731  tfis2f  7734  tfinds  7738  tfinds2  7742  tfinds3  7743  funcnvuni  7810  f1oweALT  7847  funeldmdif  7921  f1o2ndf1  7994  poxp  8000  soxp  8001  fnse  8005  suppimacnv  8021  suppcoss  8054  mpoxopynvov0g  8061  reldmtpos  8081  rntpos  8086  fpr3g  8132  frrlem9  8141  frrlem10  8142  frrlem12  8144  frrlem13  8145  wfrlem14OLD  8184  wfrlem15OLD  8185  onfununi  8203  smoiun  8223  tfrlem1  8238  tfr3  8261  frsucmptn  8301  tz7.49  8307  oaordi  8408  oawordeulem  8416  omeulem1  8444  oeordi  8449  oelimcl  8462  nnaordi  8480  nneob  8517  omsmolem  8518  erdisj  8581  qsss  8598  uniinqs  8617  fsetfcdm  8679  map0g  8703  resixpfo  8755  ixpsnf1o  8757  xpdom3  8895  mapdom3  8974  ssfiALT  8995  phplem2  9029  php3  9033  phplem4OLD  9041  php3OLD  9045  0sdom1dom  9059  sdom1  9063  unxpdomlem3  9073  findcard2OLD  9100  findcard3  9101  frfi  9103  isfiniteg  9118  xpfi  9129  fiint  9135  finsschain  9170  dffi2  9226  marypha1lem  9236  marypha2  9242  supmo  9255  suplub2  9264  infmo  9298  ordiso2  9318  ordtypelem7  9327  ordtypelem8  9328  brwdom2  9376  unxpwdom2  9391  ixpiunwdom  9393  elirrv  9399  suc11reg  9421  noinfep  9462  cantnfle  9473  cantnflem1  9491  cantnf  9495  trcl  9530  epfrs  9533  frmin  9551  frind  9552  frins2f  9555  rankpwi  9625  rankunb  9652  rankuni2b  9655  rankxplim3  9683  cplem1  9691  karden  9697  carddom2  9779  fseqenlem2  9827  ac10ct  9836  acni2  9848  acndom  9853  infpwfien  9864  alephordi  9876  alephord  9877  iunfictbso  9916  aceq3lem  9922  dfac5  9930  dfac2b  9932  dfac12lem3  9947  dfac12r  9948  cdainflem  9989  cfub  10051  cfeq0  10058  coflim  10063  cfslb2n  10070  cofsmo  10071  coftr  10075  infpssr  10110  fin23lem7  10118  fin23lem11  10119  fin23lem21  10141  isf32lem2  10156  isf34lem4  10179  isfin1-2  10187  isfin1-3  10188  fin1a2lem9  10210  fin1a2lem11  10212  fin1a2lem12  10213  fin1a2lem13  10214  domtriomlem  10244  axdc3lem2  10253  axcclem  10259  ac6c4  10283  zorn2lem4  10301  zorn2lem5  10302  zorn2lem7  10304  ttukeylem5  10315  ttukeyg  10319  brdom6disj  10334  fnrndomg  10338  iunfo  10341  iundom2g  10342  ficard  10367  konigthlem  10370  alephval2  10374  pwcfsdom  10385  fpwwe2lem8  10440  fpwwe2lem10  10442  fpwwe2lem11  10443  fpwwe2lem12  10444  pwfseqlem3  10462  gchpwdom  10472  winalim2  10498  gchina  10501  wunex2  10540  tskr1om2  10570  tskxpss  10574  inar1  10577  tskuni  10585  gruun  10608  grudomon  10619  grur1  10622  ltmpi  10706  ltexprlem2  10839  ltexprlem6  10843  reclem2pr  10850  reclem3pr  10851  reclem4pr  10852  suplem1pr  10854  mulgt0sr  10907  supsrlem  10913  axrrecex  10965  axpre-sup  10971  ltlen  11122  addid0  11440  negn0  11450  negf1o  11451  mulge0b  11891  supaddc  11988  supadd  11989  supmul1  11990  supmullem1  11991  supmullem2  11992  supmul  11993  cju  12015  nnsub  12063  0mnnnnn0  12311  un0addcl  12312  un0mulcl  12313  nn0sub  12329  nn0n0n1ge2b  12347  zle0orge1  12382  peano5uzi  12455  eluzuzle  12637  zsupss  12723  elpq  12761  qbtwnre  12979  xrsupexmnf  13085  xrinfmexpnf  13086  xrsupsslem  13087  xrinfmsslem  13088  xrub  13092  supxrun  13096  ixxdisj  13140  icodisj  13254  difreicc  13262  uzsubsubfz  13324  fzadd2  13337  elfzmlbp  13413  fzofzim  13480  elfznelfzo  13538  injresinj  13554  subfzo0  13555  flval3  13581  modirr  13708  modsumfzodifsn  13710  addmodlteq  13712  ssnn0fi  13751  seqf1o  13810  expcl2lem  13840  expnegz  13863  expaddz  13873  expmulz  13875  facwordi  14049  faclbnd4lem4  14056  bccl  14082  hashnfinnn0  14121  hashgt12el  14182  hashgt12el2  14183  hashfun  14197  hashbclem  14209  hashbc  14210  hashfacen  14211  hashfacenOLD  14212  hashf1lem1  14213  hashf1lem1OLD  14214  hashf1  14216  hash2pwpr  14235  fundmge2nop0  14251  fi1uzind  14256  brfi1indALT  14259  swrdnd0  14415  wrdind  14480  wrd2ind  14481  swrdccatin1  14483  swrdccatin2  14487  pfxccat3  14492  pfxccat3a  14496  swrdccat3blem  14497  reuccatpfxs1  14505  cshw1  14580  cshwcsh2id  14586  wwlktovfo  14718  s3iunsndisj  14724  rtrclreclem3  14816  dfrtrcl2  14818  sqrlem1  14999  sqrlem6  15004  rexanre  15103  cau3lem  15111  2clim  15326  summo  15474  fsum2dlem  15527  fsumiun  15578  prodmo  15691  fprod2dlem  15735  bpolycl  15807  rpnnen2lem12  15979  odd2np1lem  16094  oddge22np1  16103  sqoddm1div8z  16108  sumeven  16141  pwp1fsum  16145  bitsfzo  16187  sadcaddlem  16209  gcd0id  16271  algcvgblem  16327  lcmfunsnlem1  16387  lcmfunsnlem2lem1  16388  lcmfunsnlem2  16390  coprmproddvdslem  16412  divgcdcoprm0  16415  isprm7  16458  prmdvdsexpr  16467  prmfac1  16471  qnumdencl  16488  hashdvds  16521  prm23lt5  16560  pcneg  16620  prmpwdvds  16650  prmreclem2  16663  4sqlem12  16702  vdwlem6  16732  vdwlem10  16736  vdwlem13  16739  0ram  16766  ram0  16768  ramz  16771  ramcl  16775  prmgaplem3  16799  prmgaplem4  16800  prmgaplem5  16801  prmgaplem6  16802  cshwshashlem1  16842  prmlem0  16852  firest  17188  imasaddfnlem  17284  imasvscafn  17293  mremre  17358  cicsym  17561  initoid  17761  termoid  17762  iszeroi  17769  drsdirfi  18068  odupos  18091  pospo  18108  joinfval  18136  meetfval  18150  lubun  18278  acsfiindd  18316  psss  18343  mnd1id  18472  0subm  18501  insubm  18502  sursubmefmnd  18580  injsubmefmnd  18581  smndex1mgm  18591  pwmnd  18621  dfgrp2e  18650  dfgrp3lem  18718  symgfix2  19069  f1omvdco2  19101  symggen  19123  odcau  19254  pgpfi  19255  sylow2blem3  19272  sylow3lem2  19278  lsmmod  19326  efgsfo  19390  frgpuptinv  19422  frgpnabllem1  19519  cyggeninv  19528  lt6abl  19541  cyggex2  19543  gsumval3lem2  19552  gsumval3  19553  gsum2d2  19620  dmdprdd  19647  dprd2da  19690  pgpfac1lem5  19727  pgpfac  19732  srgbinomlem4  19824  dvdsrtr  19939  dvdsrmul1  19940  lss1d  20270  lspsolvlem  20449  lspsnat  20452  lbsextlem2  20466  lbsextlem3  20467  0ring  20586  01eq0ring  20588  0ring01eqbi  20589  rng1nfld  20594  domnmuln0  20614  abvn0b  20618  xrsdsreclblem  20689  qsssubdrg  20702  prmirredlem  20739  cygznlem3  20822  obslbs  20982  dsmmacl  20993  lindfrn  21073  lmiclbs  21089  lmisfree  21094  mvrf1  21239  mplcoe5lem  21285  opsrtoslem2  21308  cply1mul  21510  coe1fzgsumdlem  21517  gsummoncoe1  21520  pf1ind  21566  evl1gsumdlem  21567  matecl  21619  mat1dimelbas  21665  scmateALT  21706  mdetdiaglem  21792  mdet0  21800  mdetunilem9  21814  gsummatr01  21853  cpmatmcllem  21912  m2cpminvid2lem  21948  pmatcollpw3fi1lem2  21981  chfacfscmul0  22052  chfacfpmmul0  22056  cayhamlem3  22081  tgcl  22164  tgidm  22175  indistopon  22196  fctop  22199  cctop  22201  ppttop  22202  pptbas  22203  epttop  22204  opnnei  22316  neiptopnei  22328  tgrest  22355  restntr  22378  perfopn  22381  ordtrest2lem  22399  isreg2  22573  lmmo  22576  ordthauslem  22579  cmpsublem  22595  cmpsub  22596  cmpcld  22598  hauscmplem  22602  iunconnlem  22623  unconn  22625  2ndcrest  22650  2ndcctbss  22651  2ndcdisj  22652  dis2ndc  22656  locfincmp  22722  comppfsc  22728  txbas  22763  ptbasin  22773  ptbasfi  22777  txcls  22800  txbasval  22802  ptpjopn  22808  ptclsg  22811  dfac14lem  22813  xkoccn  22815  txcnp  22816  txindis  22830  txdis1cn  22831  tx1stc  22846  tx2ndc  22847  txkgen  22848  xkoco1cn  22853  xkoco2cn  22854  xkococn  22856  xkoinjcn  22883  txconn  22885  fbfinnfr  23037  opnfbas  23038  filtop  23051  isfild  23054  fbunfip  23065  filconn  23079  fbasrn  23080  filuni  23081  isufil2  23104  filssufilg  23107  ufileu  23115  filufint  23116  rnelfmlem  23148  rnelfm  23149  fmfnfmlem2  23151  fmfnfmlem4  23153  fmfnfm  23154  hausflimi  23176  hauspwpwf1  23183  flffbas  23191  flftg  23192  alexsublem  23240  alexsubALTlem1  23243  alexsubALTlem2  23244  alexsubALTlem3  23245  alexsubALTlem4  23246  alexsubALT  23247  ptcmplem3  23250  cldsubg  23307  qustgpopn  23316  tgptsmscld  23347  tsmsxplem1  23349  ustfilxp  23409  imasdsf1olem  23571  bldisj  23596  xbln0  23612  prdsxmslem2  23730  xrsblre  24019  icccmplem2  24031  reconn  24036  opnreen  24039  xrge0tsms  24042  metdsre  24061  iccpnfcnv  24152  cnheiborlem  24162  phtpc01  24204  pi1blem  24247  tcphcph  24446  cfilfcls  24483  iscau4  24488  bcthlem5  24537  bcth3  24540  cmssmscld  24559  hlhil  24652  ovolctb  24699  ovoliunlem2  24712  ovoliunnul  24716  ovolicc2  24731  volfiniun  24756  iundisj  24757  dyadmax  24807  dyadmbllem  24808  vitalilem2  24818  ismbfd  24848  mbfimaopnlem  24864  itg11  24900  i1faddlem  24902  mbfi1fseqlem4  24928  bddmulibl  25048  limciun  25103  perfdvf  25112  rolle  25199  dvivthlem1  25217  dvne0  25220  lhop1  25223  lhop2  25224  itgsubst  25258  dvdsq1p  25370  fta1g  25377  dgrco  25481  plydivex  25502  fta1  25513  ulmcaulem  25598  abelthlem2  25636  pilem2  25656  cxpmul2z  25891  cxpcn3lem  25945  xrlimcnp  26163  jensen  26183  wilthlem2  26263  wilthlem3  26264  muval2  26328  sqf11  26333  ppiublem1  26395  fsumvma  26406  lgsdir2lem2  26519  lgsdir2lem5  26522  lgsqrmodndvds  26546  gausslemma2dlem1a  26558  gausslemma2dlem3  26561  gausslemma2d  26567  2lgsoddprmlem2  26602  2sqreultlem  26640  2sqreunnltlem  26643  2sqreulem3  26646  dchrisum0fno1  26704  pntlem3  26802  pntleml  26804  ostthlem1  26820  ostth2lem2  26827  colinearalg  27323  axcontlem2  27378  axcontlem8  27384  edgupgr  27549  umgrpredgv  27555  numedglnl  27559  ausgrumgri  27582  ausgrusgri  27583  ushgredgedg  27641  ushgredgedgloop  27643  uhgr0v0e  27650  subumgredg2  27697  uhgrspansubgrlem  27702  uhgrspan1  27715  upgrreslem  27716  umgrreslem  27717  upgrres1  27725  fusgrfisstep  27741  nbuhgr  27755  nbuhgr2vtx1edgblem  27763  nbuhgr2vtx1edgb  27764  uhgrnbgr0nb  27766  edgnbusgreu  27779  nbusgredgeu0  27780  nbusgrf1o0  27781  nbusgrvtxm1uvtx  27817  cusgredg  27836  cusgrfi  27870  usgredgsscusgredg  27871  1loopgrnb0  27914  usgrvd0nedg  27945  uhgrvd00  27946  upgriswlk  28053  upgrwlkcompim  28055  uspgr2wlkeq  28058  uspgr2wlkeqi  28060  wlkv0  28063  wlklenvclwlkOLD  28068  wlkp1lem6  28091  lfgrwlkprop  28100  2pthnloop  28144  spthdep  28147  upgrwlkdvdelem  28149  usgr2wlkneq  28169  usgr2trlncl  28173  pthdlem1  28179  pthdlem2lem  28180  clwlkl1loop  28196  crctcshwlkn0lem3  28222  crctcshwlkn0lem5  28224  crctcshwlkn0  28231  0enwwlksnge1  28274  wlkiswwlks2  28285  wlkiswwlksupgr2  28287  wspthsnonn0vne  28327  umgr2adedgspth  28358  clwlkclwwlklem2a4  28406  clwlkclwwlklem2  28409  clwlkclwwlkf  28417  clwlkclwwlkfo  28418  erclwwlktr  28431  clwwlkf1  28458  erclwwlkntr  28480  hashecclwwlkn1  28486  umgrhashecclwwlk  28487  clwwlknonex2e  28519